diff --git a/tests/arch/ecp5/lutram.ys b/tests/arch/ecp5/lutram.ys index 9bef37c68..226d8932c 100644 --- a/tests/arch/ecp5/lutram.ys +++ b/tests/arch/ecp5/lutram.ys @@ -7,6 +7,8 @@ memory opt -full miter -equiv -flatten -make_assert -make_outputs gold gate miter +formalff -clk2ff +formalff -clk2ff sat -verify -prove-asserts -seq 5 -set-init-zero -show-inputs -show-outputs miter design -load postopt diff --git a/tests/arch/gowin/lutram.ys b/tests/arch/gowin/lutram.ys index d668783a2..15fe70945 100644 --- a/tests/arch/gowin/lutram.ys +++ b/tests/arch/gowin/lutram.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 5 -set-init-zero -show-inputs -show-outputs miter sat -prove-asserts -seq 5 -set-init-zero -show-inputs -show-outputs miter diff --git a/tests/arch/ice40/fsm.ys b/tests/arch/ice40/fsm.ys index d01c58e04..1427143ba 100644 --- a/tests/arch/ice40/fsm.ys +++ b/tests/arch/ice40/fsm.ys @@ -6,6 +6,7 @@ flatten equiv_opt -run :prove -map +/ice40/cells_sim.v synth_ice40 formalff -clk2ff miter -equiv -make_assert -flatten gold gate miter +formalff -clk2ff sat -verify -prove-asserts -show-public -set-at 1 in_reset 1 -seq 20 -prove-skip 1 miter design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) diff --git a/tests/arch/intel_alm/lutram.ys b/tests/arch/intel_alm/lutram.ys index 4e77afded..bceb6abc3 100644 --- a/tests/arch/intel_alm/lutram.ys +++ b/tests/arch/intel_alm/lutram.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 @@ -28,6 +29,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/arch/machxo2/lutram.ys b/tests/arch/machxo2/lutram.ys index 65af7b2c2..fdeb61e15 100644 --- a/tests/arch/machxo2/lutram.ys +++ b/tests/arch/machxo2/lutram.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 5 -set-init-zero -show-inputs -show-outputs miter design -load postopt diff --git a/tests/arch/nanoxplore/lutram.ys b/tests/arch/nanoxplore/lutram.ys index 61b813bfb..3101b90a4 100644 --- a/tests/arch/nanoxplore/lutram.ys +++ b/tests/arch/nanoxplore/lutram.ys @@ -31,6 +31,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 @@ -53,6 +54,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 @@ -73,6 +75,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 @@ -93,6 +96,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 @@ -136,6 +140,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/arch/nexus/lutram.ys b/tests/arch/nexus/lutram.ys index 6e33431b6..b86663318 100644 --- a/tests/arch/nexus/lutram.ys +++ b/tests/arch/nexus/lutram.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 5 -set-init-zero -show-inputs -show-outputs miter design -load postopt diff --git a/tests/arch/quicklogic/pp3/fsm.ys b/tests/arch/quicklogic/pp3/fsm.ys index 3276e45c6..4b99562fc 100644 --- a/tests/arch/quicklogic/pp3/fsm.ys +++ b/tests/arch/quicklogic/pp3/fsm.ys @@ -6,6 +6,7 @@ flatten equiv_opt -run :prove -map +/quicklogic/pp3/cells_sim.v -map +/quicklogic/common/cells_sim.v synth_quicklogic async2sync miter -equiv -make_assert -flatten gold gate miter +formalff -clk2ff sat -verify -prove-asserts -show-public -set-at 1 in_reset 1 -seq 20 -prove-skip 1 miter design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) diff --git a/tests/arch/xilinx/lutram.ys b/tests/arch/xilinx/lutram.ys index 34caa8c6c..a5594b009 100644 --- a/tests/arch/xilinx/lutram.ys +++ b/tests/arch/xilinx/lutram.ys @@ -7,6 +7,7 @@ #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 @@ -27,6 +28,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 @@ -47,6 +49,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 @@ -68,6 +71,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 @@ -88,6 +92,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 @@ -108,6 +113,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 @@ -128,6 +134,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 @@ -148,6 +155,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