From cf2431ac2d48632559ef6ee2cae96460d8ee2da4 Mon Sep 17 00:00:00 2001 From: "Emil J. Tywoniak" Date: Sat, 7 Feb 2026 00:52:45 +0100 Subject: [PATCH] xilinx: fix tests --- tests/arch/xilinx/macc.ys | 2 ++ tests/arch/xilinx/pmgen_xilinx_srl.ys | 2 ++ 2 files changed, 4 insertions(+) diff --git a/tests/arch/xilinx/macc.ys b/tests/arch/xilinx/macc.ys index 61a570f48..ab6bcc40e 100644 --- a/tests/arch/xilinx/macc.ys +++ b/tests/arch/xilinx/macc.ys @@ -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 diff --git a/tests/arch/xilinx/pmgen_xilinx_srl.ys b/tests/arch/xilinx/pmgen_xilinx_srl.ys index 9a5e70ea9..885f9e5a4 100644 --- a/tests/arch/xilinx/pmgen_xilinx_srl.ys +++ b/tests/arch/xilinx/pmgen_xilinx_srl.ys @@ -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