diff --git a/tests/aiger/run-test.sh b/tests/aiger/run-test.sh index 94d83ede4..7ec743adb 100755 --- a/tests/aiger/run-test.sh +++ b/tests/aiger/run-test.sh @@ -32,6 +32,7 @@ prep design -stash gate design -import gold -as gold design -import gate -as gate +formalff -clk2ff miter -equiv -flatten -make_assert -make_outputs gold gate miter sat -verify -prove-asserts -show-ports -seq 16 miter " -l ${aag}.log @@ -49,6 +50,7 @@ prep design -stash gate design -import gold -as gold design -import gate -as gate +formalff -clk2ff miter -equiv -flatten -make_assert -make_outputs gold gate miter sat -verify -prove-asserts -show-ports -seq 16 miter " -l ${aig}.log diff --git a/tests/arch/ecp5/dpram.ys b/tests/arch/ecp5/dpram.ys index 3bc6bc1d0..7dcc04f2a 100644 --- a/tests/arch/ecp5/dpram.ys +++ b/tests/arch/ecp5/dpram.ys @@ -10,6 +10,7 @@ miter -equiv -flatten -make_assert -make_outputs gold gate miter #Blocked by issue #1358 (Missing ECP5 simulation models) #ERROR: Failed to import cell gate.mem.0.0.0 (type DP16KD) to SAT database. +#formalff -clk2ff #sat -verify -prove-asserts -seq 3 -set-init-zero -show-inputs -show-outputs miter design -load postopt diff --git a/tests/arch/ice40/dpram.ys b/tests/arch/ice40/dpram.ys index 4f6a253ea..0cb935175 100644 --- a/tests/arch/ice40/dpram.ys +++ b/tests/arch/ice40/dpram.ys @@ -7,6 +7,7 @@ memory opt -full miter -equiv -flatten -make_assert -make_outputs gold gate miter +formalff -clk2ff sat -verify -prove-asserts -seq 3 -set-init-zero -show-inputs -show-outputs miter design -load postopt diff --git a/tests/fsm/generate.py b/tests/fsm/generate.py index 784e5a054..bcf34c95d 100644 --- a/tests/fsm/generate.py +++ b/tests/fsm/generate.py @@ -116,5 +116,6 @@ for idx in range(args.count): print('opt; wreduce; share%s; opt; fsm;;' % random.choice(['', ' -aggressive'])) print('cd ..') print('miter -equiv -flatten -ignore_gold_x -make_outputs -make_outcmp gold gate miter') + print('formalff -clk2ff') print('sat -verify-no-timeout -timeout 20 -seq 5 -set-at 1 %s_rst 1 -prove trigger 0 -prove-skip 1 -show-inputs -show-outputs miter' % ('gold' if rst2 else 'in')) diff --git a/tests/liberty/read_liberty.ys b/tests/liberty/read_liberty.ys index 7cbb0a19d..430ea6138 100644 --- a/tests/liberty/read_liberty.ys +++ b/tests/liberty/read_liberty.ys @@ -4,6 +4,7 @@ read_verilog retention.lib.verilogsim proc rename retention_cell retention_cell_vlog async2sync +formalff -clk2ff equiv_make retention_cell_lib retention_cell_vlog equiv equiv_induct equiv equiv_status -assert equiv diff --git a/tests/opt/opt_dff_dffmux.ys b/tests/opt/opt_dff_dffmux.ys index 43190cc31..214580218 100644 --- a/tests/opt/opt_dff_dffmux.ys +++ b/tests/opt/opt_dff_dffmux.ys @@ -6,7 +6,7 @@ endmodule EOT proc -equiv_opt -assert opt +equiv_opt -formalff -assert opt design -load postopt select -assert-count 1 t:$dffe r:WIDTH=2 %i select -assert-count 0 t:$dffe %% t:* %D @@ -21,7 +21,7 @@ endmodule EOT proc -equiv_opt -assert opt +equiv_opt -formalff -assert opt design -load postopt wreduce select -assert-count 1 t:$dffe r:WIDTH=2 %i @@ -37,7 +37,7 @@ endmodule EOT proc -equiv_opt -assert opt +equiv_opt -formalff -assert opt design -load postopt select -assert-count 1 t:$dffe r:WIDTH=2 %i select -assert-count 0 t:$dffe %% t:* %D @@ -52,7 +52,7 @@ endmodule EOT proc -equiv_opt -assert opt +equiv_opt -formalff -assert opt design -load postopt select -assert-count 1 t:$dffe r:WIDTH=4 %i select -assert-count 0 t:$dffe %% t:* %D @@ -67,7 +67,7 @@ endmodule EOT proc -equiv_opt -assert opt +equiv_opt -formalff -assert opt design -load postopt wreduce select -assert-count 1 t:$sdffe r:WIDTH=2 %i @@ -86,7 +86,7 @@ endmodule EOT proc -equiv_opt -assert opt +equiv_opt -formalff -assert opt design -load postopt wreduce select -assert-count 1 t:$sdffe r:WIDTH=2 %i @@ -122,6 +122,7 @@ design -stash gate design -import gold -as gold design -import gate -as gate miter -equiv -flatten -make_assert -make_outputs gold gate miter +formalff -clk2ff sat -tempinduct -verify -prove-asserts -show-ports miter design -load gate diff --git a/tests/sat/asserts.ys b/tests/sat/asserts.ys index 7df8dade3..58414f19c 100644 --- a/tests/sat/asserts.ys +++ b/tests/sat/asserts.ys @@ -1,3 +1,3 @@ read_verilog -sv asserts.v -hierarchy; proc; opt; async2sync +hierarchy; proc; opt; async2sync; formalff -clk2ff sat -verify -seq 1 -set-at 1 rst 1 -tempinduct -prove-asserts diff --git a/tests/sat/asserts_seq.ys b/tests/sat/asserts_seq.ys index db94f94ea..eb3163691 100644 --- a/tests/sat/asserts_seq.ys +++ b/tests/sat/asserts_seq.ys @@ -1,5 +1,5 @@ read_verilog -sv asserts_seq.v -hierarchy; proc; opt; async2sync +hierarchy; proc; opt; async2sync; formalff -clk2ff sat -verify -prove-asserts -tempinduct -seq 1 test_001 sat -falsify -prove-asserts -tempinduct -seq 1 test_002 diff --git a/tests/sat/counters-repeat.ys b/tests/sat/counters-repeat.ys index b3dcfe08a..4e120a42b 100644 --- a/tests/sat/counters-repeat.ys +++ b/tests/sat/counters-repeat.ys @@ -4,6 +4,7 @@ proc; opt expose -shared counter1 counter2 miter -equiv -make_assert -make_outputs counter1 counter2 miter +formalff -clk2ff cd miter; flatten; opt sat -verify -prove-asserts -tempinduct -set-at 1 in_rst 1 -seq 1 -show-inputs -show-outputs diff --git a/tests/sat/counters.ys b/tests/sat/counters.ys index 330895f82..d5c5374e3 100644 --- a/tests/sat/counters.ys +++ b/tests/sat/counters.ys @@ -4,6 +4,7 @@ proc; opt expose -shared counter1 counter2 miter -equiv -make_assert -make_outputs counter1 counter2 miter +formalff -clk2ff cd miter; flatten; opt sat -verify -prove-asserts -tempinduct -set-at 1 in_rst 1 -seq 1 -show-inputs -show-outputs diff --git a/tests/sat/dff.ys b/tests/sat/dff.ys index ba3625871..7c71a4f32 100644 --- a/tests/sat/dff.ys +++ b/tests/sat/dff.ys @@ -18,4 +18,4 @@ endmodule EOT # This ensures that 1) coarse cells have SAT models, 2) fine cells have SAT models, 3) they're equivalent -equiv_opt -assert simplemap +equiv_opt -formalff -assert simplemap diff --git a/tests/svtypes/enum_simple.ys b/tests/svtypes/enum_simple.ys index 36922f5e0..3bd311962 100644 --- a/tests/svtypes/enum_simple.ys +++ b/tests/svtypes/enum_simple.ys @@ -1,5 +1,5 @@ read_verilog -sv enum_simple.sv -hierarchy; proc; opt; async2sync +hierarchy; proc; opt; async2sync; formalff -clk2ff sat -verify -seq 1 -set-at 1 rst 1 -tempinduct -prove-asserts -show-all diff --git a/tests/techmap/dfflibmap_formal.ys b/tests/techmap/dfflibmap_formal.ys index 71a52a261..c156cae46 100644 --- a/tests/techmap/dfflibmap_formal.ys +++ b/tests/techmap/dfflibmap_formal.ys @@ -1,3 +1,4 @@ +#TODO formalff shouldn't be used here. Instead, we should use SAT ################################################################## read_verilog -sv -icells <