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.
---
 manual/CHAPTER_CellLib.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'manual/CHAPTER_CellLib.tex')

diff --git a/manual/CHAPTER_CellLib.tex b/manual/CHAPTER_CellLib.tex
index 3c9fb31cc..86b1f6a9a 100644
--- a/manual/CHAPTER_CellLib.tex
+++ b/manual/CHAPTER_CellLib.tex
@@ -603,7 +603,7 @@ Add information about {\tt \$specify2}, {\tt \$specify3}, and {\tt \$specrule} c
 
 \begin{fixme}
 Add information about {\tt \$assert}, {\tt \$assume}, {\tt \$live}, {\tt \$fair}, {\tt \$cover}, {\tt \$equiv},
-{\tt \$initstate}, {\tt \$anyconst}, {\tt \$anyseq}, {\tt \$allconst}, {\tt \$allseq} cells.
+{\tt \$initstate}, {\tt \$anyconst}, {\tt \$anyseq}, {\tt \$anyinit}, {\tt \$allconst}, {\tt \$allseq} cells.
 \end{fixme}
 
 \begin{fixme}
-- 
cgit v1.2.3

