From c0063288d699f4f3edf5e0ff6ee1bd5cfa9ac884 Mon Sep 17 00:00:00 2001
From: Jannis Harder <me@jix.one>
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/fsm/fsm_detect.cc | 1 +
 1 file changed, 1 insertion(+)

(limited to 'passes/fsm')

diff --git a/passes/fsm/fsm_detect.cc b/passes/fsm/fsm_detect.cc
index a2d38a0bd..f829714c4 100644
--- a/passes/fsm/fsm_detect.cc
+++ b/passes/fsm/fsm_detect.cc
@@ -280,6 +280,7 @@ struct FsmDetectPass : public Pass {
 
 		CellTypes ct;
 		ct.setup_internals();
+		ct.setup_internals_anyinit();
 		ct.setup_internals_mem();
 		ct.setup_stdcells();
 		ct.setup_stdcells_mem();
-- 
cgit v1.2.3