Add $allconst and $allseq cell types

Signed-off-by: Clifford Wolf <clifford@clifford.at>

1 files changed, 7 insertions, 2 deletions

diff --git a/README.md b/README.md
index 92dc68a6a..87b231a5c 100644
--- a/README.md
+++ b/README.md
@@ -387,15 +387,20 @@ Non-standard or SystemVerilog features for formal verification
 - The system task ``$initstate`` evaluates to 1 in the initial state and
   to 0 otherwise.
 
-- The system task ``$anyconst`` evaluates to any constant value. This is
+- The system function ``$anyconst`` evaluates to any constant value. This is
   equivalent to declaring a reg as ``rand const``, but also works outside
   of checkers. (Yosys also supports ``rand const`` outside checkers.)
 
-- The system task ``$anyseq`` evaluates to any value, possibly a different
+- The system function ``$anyseq`` evaluates to any value, possibly a different
   value in each cycle. This is equivalent to declaring a reg as ``rand``,
   but also works outside of checkers. (Yosys also supports ``rand``
   variables outside checkers.)
 
+- The system functions ``$allconst`` and ``$allseq`` are used to construct formal
+  exist-forall problems. Assertions are only violated if the trace vialoates
+  the assertion for all ``$allconst/$allseq`` values and assumptions only hold
+  if the trace satisfies the assumtion for all ``$allconst/$allseq`` values.
+
 - The SystemVerilog tasks ``$past``, ``$stable``, ``$rose`` and ``$fell`` are
   supported in any clocked block.