From: Clifford Wolf <clifford@clifford.at>
Date: Fri, 14 Oct 2016 13:39:33 +0000 (+0200)
Subject: Added notes about some formal features to README
X-Git-Tag: yosys-0.7~27
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=512f93f8663dc438c2afa35872fa3b39b87e5323;p=yosys.git

Added notes about some formal features to README
---

diff --git a/README b/README
index 32e9ba24a..8e43d4446 100644
--- a/README
+++ b/README
@@ -374,6 +374,27 @@ Verilog Attributes and non-standard features
   and constant values). The intended use for this is synthesis-time DRC.
 
 
+Non-standard or SystemVerilog features for formal verification
+==============================================================
+
+- Support for "assert", "assume", and "restrict" is enabled when
+  read_verilog is called with -formal.
+
+- The system task $initstate evaluates to 1 in the initial state and
+  to 0 otherwise.
+
+- The system task $anyconst evaluates to any constant value.
+
+- The system task $anyseq evaluates to any value, possibly a different
+  value in each cycle.
+
+- The SystemVerilog tasks $past, $stable, $rose and $fell are supported
+  in any clocked block.
+
+- The syntax @($global_clock) can be used to create FFs that have no
+  explicit clock input ($ff cells).
+
+
 Supported features from SystemVerilog
 =====================================
 
@@ -384,8 +405,8 @@ from SystemVerilog:
   form. In module context: "assert property (<expression>);" and within an
   always block: "assert(<expression>);". It is transformed to a $assert cell.
 
-- The "assume" statements from SystemVerilog are also supported. The same
-  limitations as with the "assert" statement apply.
+- The "assume" and "restrict" statements from SystemVerilog are also
+  supported. The same limitations as with the "assert" statement apply.
 
 - The keywords "always_comb", "always_ff" and "always_latch", "logic" and
   "bit" are supported.