From c0063288d699f4f3edf5e0ff6ee1bd5cfa9ac884 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Thu, 21 Jul 2022 14:22:15 +0200 Subject: Add the $anyinit cell and the formalff pass These can be used to protect undefined flip-flop initialization values from optimizations that are not sound for formal verification and can help mapping all solver-provided values in witness traces for flows that use different backends simultaneously. --- passes/opt/opt_clean.cc | 2 ++ 1 file changed, 2 insertions(+) (limited to 'passes/opt/opt_clean.cc') diff --git a/passes/opt/opt_clean.cc b/passes/opt/opt_clean.cc index cb2c261c4..dde7c5299 100644 --- a/passes/opt/opt_clean.cc +++ b/passes/opt/opt_clean.cc @@ -633,6 +633,7 @@ struct OptCleanPass : public Pass { keep_cache.reset(design); ct_reg.setup_internals_mem(); + ct_reg.setup_internals_anyinit(); ct_reg.setup_stdcells_mem(); ct_all.setup(design); @@ -694,6 +695,7 @@ struct CleanPass : public Pass { keep_cache.reset(design); ct_reg.setup_internals_mem(); + ct_reg.setup_internals_anyinit(); ct_reg.setup_stdcells_mem(); ct_all.setup(design); -- cgit v1.2.3