github.com/YosysHQ.yosys
1
0
Fork 0
mirror of synced 2026-05-19 20:27:38 +00:00
Code Issues Releases Wiki Activity

xilinx: fix tests

Browse Source
This commit is contained in:
Emil J. Tywoniak
2026-02-07 00:52:45 +01:00
parent 6882eb670a
commit cf2431ac2d
2 changed files with 4 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
tests/arch/xilinx/macc.ys
View File

@@ -6,6 +6,7 @@ proc
#equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad ### TODO
equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -noiopad
miter -equiv -flatten -make_assert -make_outputs gold gate miter
formalff -clk2ff
sat -verify -prove-asserts -seq 3 -show-inputs -show-outputs miter
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd macc # Constrain all select calls below inside the top module
@@ -20,6 +21,7 @@ proc
#equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad ### TODO
equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -noiopad
miter -equiv -flatten -make_assert -make_outputs gold gate miter
formalff -clk2ff
sat -verify -prove-asserts -seq 4 -show-inputs -show-outputs miter
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd macc2 # Constrain all select calls below inside the top module

2
tests/arch/xilinx/pmgen_xilinx_srl.ys
View File

@@ -35,6 +35,7 @@ design -stash gate
design -copy-from gold -as gold pmtest_xilinx_srl_pm_fixed
design -copy-from gate -as gate pmtest_xilinx_srl_pm_fixed
formalff -clk2ff
miter -equiv -flatten -make_assert gold gate miter
sat -set-init-zero -seq 5 -verify -prove-asserts miter
@@ -51,5 +52,6 @@ design -stash gate
design -copy-from gold -as gold pmtest_xilinx_srl_pm_variable
design -copy-from gate -as gate pmtest_xilinx_srl_pm_variable
formalff -clk2ff
miter -equiv -flatten -make_assert gold gate miter
sat -set-init-zero -seq 5 -verify -prove-asserts miter