From 2e6d112a2d458520fdca1b3cf021dfd6a1dded79 Mon Sep 17 00:00:00 2001 From: "Emil J. Tywoniak" Date: Fri, 6 Feb 2026 23:16:21 +0100 Subject: [PATCH] tests: add formalff -clk2ff to fpga fsm.ys --- tests/arch/anlogic/fsm.ys | 1 + tests/arch/ecp5/fsm.ys | 1 + tests/arch/efinix/fsm.ys | 1 + tests/arch/fabulous/fsm.ys | 1 + tests/arch/gatemate/fsm.ys | 1 + tests/arch/gowin/fsm.ys | 1 + tests/arch/ice40/fsm.ys | 1 + tests/arch/intel_alm/fsm.ys | 1 + tests/arch/machxo2/fsm.ys | 1 + tests/arch/nanoxplore/fsm.ys | 1 + tests/arch/nexus/fsm.ys | 1 + tests/arch/xilinx/fsm.ys | 2 ++ 12 files changed, 13 insertions(+) diff --git a/tests/arch/anlogic/fsm.ys b/tests/arch/anlogic/fsm.ys index eb94177ad..04c5f9831 100644 --- a/tests/arch/anlogic/fsm.ys +++ b/tests/arch/anlogic/fsm.ys @@ -5,6 +5,7 @@ flatten equiv_opt -run :prove -map +/anlogic/cells_sim.v synth_anlogic 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/ecp5/fsm.ys b/tests/arch/ecp5/fsm.ys index a77986bbc..45b96ac63 100644 --- a/tests/arch/ecp5/fsm.ys +++ b/tests/arch/ecp5/fsm.ys @@ -5,6 +5,7 @@ flatten equiv_opt -run :prove -map +/ecp5/cells_sim.v synth_ecp5 miter -equiv -make_assert -flatten gold gate miter +techmap -map +/dff2ff.v 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/efinix/fsm.ys b/tests/arch/efinix/fsm.ys index aef720d46..ba2a9a802 100644 --- a/tests/arch/efinix/fsm.ys +++ b/tests/arch/efinix/fsm.ys @@ -5,6 +5,7 @@ flatten equiv_opt -run :prove -map +/efinix/cells_sim.v synth_efinix 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/fabulous/fsm.ys b/tests/arch/fabulous/fsm.ys index 9c3831682..d1e05f044 100644 --- a/tests/arch/fabulous/fsm.ys +++ b/tests/arch/fabulous/fsm.ys @@ -6,6 +6,7 @@ flatten equiv_opt -run :prove -map +/fabulous/prims.v synth_fabulous async2sync miter -equiv -make_assert -flatten gold gate miter +formalff -clk2ff stat sat -verify -prove-asserts -show-public -set-at 1 in_reset 1 -seq 20 -prove-skip 1 miter diff --git a/tests/arch/gatemate/fsm.ys b/tests/arch/gatemate/fsm.ys index 506862c90..835ef91e2 100644 --- a/tests/arch/gatemate/fsm.ys +++ b/tests/arch/gatemate/fsm.ys @@ -6,6 +6,7 @@ flatten equiv_opt -run :prove -map +/gatemate/cells_sim.v synth_gatemate -noiopad async2sync miter -equiv -make_assert -flatten gold gate miter +formalff -clk2ff stat sat -verify -prove-asserts -show-public -set-at 1 in_reset 1 -seq 20 -prove-skip 1 miter diff --git a/tests/arch/gowin/fsm.ys b/tests/arch/gowin/fsm.ys index ce4504522..b2a6637d4 100644 --- a/tests/arch/gowin/fsm.ys +++ b/tests/arch/gowin/fsm.ys @@ -5,6 +5,7 @@ flatten equiv_opt -run :prove -map +/gowin/cells_sim.v synth_gowin # equivalency check miter -equiv -make_assert -flatten gold gate miter +formalff -clk2ff sat -verify -show-all -dump_vcd x.vcd -prove-asserts -set-at 1 in_reset 1 -seq 20 -prove-skip 1 miter #design -load postopt diff --git a/tests/arch/ice40/fsm.ys b/tests/arch/ice40/fsm.ys index e3b746202..d01c58e04 100644 --- a/tests/arch/ice40/fsm.ys +++ b/tests/arch/ice40/fsm.ys @@ -4,6 +4,7 @@ proc flatten equiv_opt -run :prove -map +/ice40/cells_sim.v synth_ice40 +formalff -clk2ff miter -equiv -make_assert -flatten gold gate miter sat -verify -prove-asserts -show-public -set-at 1 in_reset 1 -seq 20 -prove-skip 1 miter diff --git a/tests/arch/intel_alm/fsm.ys b/tests/arch/intel_alm/fsm.ys index f3060684a..1f447a8c5 100644 --- a/tests/arch/intel_alm/fsm.ys +++ b/tests/arch/intel_alm/fsm.ys @@ -6,6 +6,7 @@ flatten equiv_opt -run :prove -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclonev -noiopad -noclkbuf 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/machxo2/fsm.ys b/tests/arch/machxo2/fsm.ys index 3e10a069a..c9a7edcc5 100644 --- a/tests/arch/machxo2/fsm.ys +++ b/tests/arch/machxo2/fsm.ys @@ -5,6 +5,7 @@ flatten equiv_opt -run :prove -map +/lattice/cells_sim_xo2.v synth_lattice -family xo2 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/nanoxplore/fsm.ys b/tests/arch/nanoxplore/fsm.ys index 136b220b7..801e883b3 100644 --- a/tests/arch/nanoxplore/fsm.ys +++ b/tests/arch/nanoxplore/fsm.ys @@ -6,6 +6,7 @@ flatten equiv_opt -run :prove -map +/nanoxplore/cells_sim.v synth_nanoxplore -noiopad 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/nexus/fsm.ys b/tests/arch/nexus/fsm.ys index 24ad8fe5b..e7d511c9a 100644 --- a/tests/arch/nexus/fsm.ys +++ b/tests/arch/nexus/fsm.ys @@ -5,6 +5,7 @@ flatten equiv_opt -run :prove -map +/nexus/cells_sim.v synth_nexus 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/fsm.ys b/tests/arch/xilinx/fsm.ys index 3b1919627..c3da9a5ee 100644 --- a/tests/arch/xilinx/fsm.ys +++ b/tests/arch/xilinx/fsm.ys @@ -7,6 +7,7 @@ design -save orig equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -noiopad 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) @@ -23,6 +24,7 @@ design -load orig equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -family xc3se -noiopad 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)