From 512f93f8663dc438c2afa35872fa3b39b87e5323 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Fri, 14 Oct 2016 15:39:33 +0200
Subject: [PATCH] Added notes about some formal features to README

---
 README | 25 +++++++++++++++++++++++--
 1 file changed, 23 insertions(+), 2 deletions(-)

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.