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/sat/Makefile.inc | 1 + 1 file changed, 1 insertion(+) (limited to 'passes/sat/Makefile.inc') diff --git a/passes/sat/Makefile.inc b/passes/sat/Makefile.inc index da6d49433..ebe3dc536 100644 --- a/passes/sat/Makefile.inc +++ b/passes/sat/Makefile.inc @@ -10,6 +10,7 @@ OBJS += passes/sat/expose.o OBJS += passes/sat/assertpmux.o OBJS += passes/sat/clk2fflogic.o OBJS += passes/sat/async2sync.o +OBJS += passes/sat/formalff.o OBJS += passes/sat/supercover.o OBJS += passes/sat/fmcombine.o OBJS += passes/sat/mutate.o -- cgit v1.2.3