Commit d13c1c38 authored by Guillem's avatar Guillem
Browse files

Add formal test

BMC test of formal properties
parent aa8fcea7
This diff is collapsed.
[options]
mode bmc
#append 10
[engines]
smtbmc boolector
smtbmc
abc bmc3
#SystemVerilog
[script]
verific -vlog-define FORMAL
verific -sv MCCU.sv
verific -import -extnets -all MCCU
prep -top MCCU
#Verilog
#[script]
#read_verilog -formal MCCU.sv
#prep -top MCCU
#opt -share_all
[files]
/home/bscuser/GITLAB/multicore_pmu/lagarto-lowrisc/lagarto_modulos/AXI_PMU/MCCU/hdl/MCCU.sv
#Check that the formal properties pass
sby -f MCCU.sby
#gtkwave ./MCCU/engine_0/trace.vcd MCCU.gtkw
#Run a particular case
#sby -f MCCU_cover.sby
#Show the trace of the cover
gtkwave ./MCCU/engine_0/trace.vcd MCCU.gtkw
......@@ -19,7 +19,6 @@ double sc_time_stamp(){ //called by $time in verilog
return main_time; //converts to double , to match
}
// debug function to generate waveforms and clock
// debug function to generate waveforms and clock
void ticktoc_and_trace(VMCCU* module,VerilatedVcdC* tfp){
//waveforms and tick clock
if (tfp != NULL){
......@@ -61,8 +60,6 @@ void tick_and_trace(VMCCU* module,VerilatedVcdC* tfp){
}
}
struct TestCase {
const char* name;
bool rstn_i, enable_i;
......@@ -74,11 +71,18 @@ struct TestCase {
TestCase test_cases[] {
//name ,rstn_i ,enable_i ,events_i ,quota_i ,events_weights_i
{ "Rst " ,0 ,0 ,{0,2,0,4} ,{0,0,0,0} ,{{0,0,0,0},{5,0,0,8},{9,0,11,7},{9,6,11,11}}},
{ "Init " ,1 ,0 ,{16,16,7,7} ,{10,15,20,25} ,{{1,2,3,4},{5,6,7,8},{9,10,11,12},{13,14,15,16}}},
{ "Delay " ,1 ,0 ,{14,15,3,4} ,{10,15,20,25} ,{{1,2,3,4},{5,6,7,8},{9,10,11,12},{13,14,15,16}}},
{ "Init " ,1 ,0 ,{15,15,7,7} ,{10,15,20,25} ,{{1,2,3,4},{5,6,7,8},{9,10,11,12},{13,14,15,16}}},
{ "Delay " ,1 ,0 ,{15,15,3,4} ,{10,15,20,25} ,{{1,2,3,4},{5,6,7,8},{9,10,11,12},{13,14,15,16}}},
{ "Enable " ,1 ,1 ,{13,12,3,4} ,{10,15,20,25} ,{{1,2,3,4},{5,6,7,8},{9,10,11,12},{13,14,15,16}}},
{ "Enable " ,1 ,1 ,{1,2,3,4} ,{10,15,20,25} ,{{1,2,3,4},{5,6,7,8},{9,10,11,12},{13,14,15,16}}},
};
/*
TestCase test_cases[] {
//name ,rstn_i ,enable_i ,events_i ,quota_i ,events_weights_i
{ "Rst " ,0 ,0 ,{0,0,0,0} ,{0,0,0,0} ,{{0,0,0,0},{0,0,0,0},{9,0,11,7},{9,6,11,11}}},
{ "Init " ,1 ,0 ,{1,0,0,0} ,{0,0,0,0} ,{{512,0,0,0},{0,0,0,0},{9,10,11,12},{13,14,15,16}}},
{ "wait " ,1 ,0 ,{0,0,0,0} ,{0,0,0,0} ,{{0,0,0,0},{0,0,0,0},{9,0,11,7},{9,6,11,11}}},
};*/
int main(int argc, char **argv, char **env) {
//enable waveforms
......
[*]
[*] GTKWave Analyzer v3.3.86 (w)1999-2017 BSI
[*] Tue Jul 16 13:02:29 2019
[*] Fri Jul 19 09:37:02 2019
[*]
[dumpfile] "/home/bscuser/GITLAB/multicore_pmu/lagarto-lowrisc/lagarto_modulos/AXI_PMU/MCCU/tb/verilator/obj_dir/VMCCU.vcd"
[dumpfile_mtime] "Tue Jul 16 13:01:20 2019"
[dumpfile_size] 5624
[dumpfile_mtime] "Fri Jul 19 09:34:12 2019"
[dumpfile_size] 5508
[savefile] "/home/bscuser/GITLAB/multicore_pmu/lagarto-lowrisc/lagarto_modulos/AXI_PMU/MCCU/tb/verilator/tests.gtkw"
[timestart] 0
[size] 1920 1025
[pos] 0 27
*-2.900144 10 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1
*-2.900144 12 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1
[treeopen] TOP.
[treeopen] TOP.MCCU.
[treeopen] TOP.MCCU.GeneratedQuotaMonitor.
[sst_width] 297
[signals_width] 246
[signals_width] 573
[sst_expanded] 1
[sst_vpaned_height] 292
[sst_vpaned_height] 283
@28
[color] 3
TOP.clk_i
......@@ -34,56 +33,42 @@ TOP.events_i(0)[3:0]
(3)TOP.events_i(0)[3:0]
@1001200
-group_end
@800022
TOP.events_i(1)[3:0]
@28
(0)TOP.events_i(1)[3:0]
(1)TOP.events_i(1)[3:0]
(2)TOP.events_i(1)[3:0]
(3)TOP.events_i(1)[3:0]
@1001200
-group_end
@1000200
-Events
@24
@22
[color] 6
TOP.MCCU.ccc_suma(0)[63:0]
@23
TOP.MCCU.quota(0)[31:0]
TOP.MCCU.quota_int(0)[31:0]
@28
TOP.MCCU.interruption_quota_o(0)
@24
[color] 6
TOP.MCCU.events_weights(0)(0)[9:0]
[color] 6
TOP.MCCU.events_weights(0)(1)[9:0]
[color] 6
TOP.MCCU.events_weights(0)(2)[9:0]
[color] 6
TOP.MCCU.events_weights(0)(3)[9:0]
TOP.MCCU.ccc_suma_int(0)[63:0]
[color] 2
TOP.MCCU.ccc_suma(1)[63:0]
@22
TOP.MCCU.quota(1)[31:0]
TOP.MCCU.events_weights_int(0)(0)[9:0]
@28
TOP.MCCU.interruption_quota_o(1)
(3)TOP.events_i(0)[3:0]
@24
[color] 2
TOP.MCCU.events_weights(1)(0)[9:0]
[color] 2
TOP.MCCU.events_weights(1)(1)[9:0]
TOP.MCCU.events_weights_int(0)(1)[9:0]
@28
(2)TOP.events_i(0)[3:0]
@24
[color] 2
TOP.MCCU.events_weights(1)(2)[9:0]
TOP.MCCU.events_weights_int(0)(2)[9:0]
@29
(1)TOP.events_i(0)[3:0]
@24
[color] 2
TOP.MCCU.events_weights(1)(3)[9:0]
@22
TOP.MCCU.events_weights_int(0)(3)[9:0]
@28
(0)TOP.events_i(0)[3:0]
@24
[color] 6
TOP.MCCU.events_weights_i(0)(0)[9:0]
[color] 6
TOP.MCCU.events_weights_i(0)(1)[9:0]
[color] 6
TOP.MCCU.events_weights_i(0)(2)[9:0]
[color] 6
TOP.MCCU.events_weights_i(0)(3)[9:0]
TOP.MCCU.events_weights_i(1)(0)[9:0]
TOP.MCCU.events_weights_i(1)(1)[9:0]
TOP.MCCU.events_weights_i(1)(2)[9:0]
TOP.MCCU.events_weights_i(1)(3)[9:0]
[pattern_trace] 1
[pattern_trace] 0
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment