From: Clifford Wolf <clifford@clifford.at>
Date: Tue, 6 Mar 2018 10:19:27 +0000 (+0100)
Subject: Update verific.rst
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f151ea733a93bada9f9d3012c7d43a6dc45fc704;p=SymbiYosys.git

Update verific.rst

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

diff --git a/docs/source/verific.rst b/docs/source/verific.rst
index 74756be..6cf1ca1 100644
--- a/docs/source/verific.rst
+++ b/docs/source/verific.rst
@@ -30,10 +30,11 @@ such as
   * ``default disable iff`` ... ``;``
   * ``property`` ... ``endproperty``
   * ``sequence`` ... ``endsequence``
-  * Parameters to sequences and properties
-  * Storing sequences and properties in packages
+  * ``checker`` ... ``endchecker``
+  * Arguments to sequences, properties, and checkers
+  * Storing sequences, properties, and checkers in packages
 
-In addition the SVA-specific fetures, the SystemVerilog ``bind`` statement and
+In addition the SVA-specific features, the SystemVerilog ``bind`` statement and
 deep hierarchical references are supported, simplifying the integration of
 formal properties with the design under test.
 
@@ -44,13 +45,15 @@ SystemVerilog formal test-bench into a VHDL design under test.
 Expressions in Sequences
 ~~~~~~~~~~~~~~~~~~~~~~~~
 
-Any standard Verilog boolean expression is supported, as well as the SystemVerilog
-functions ``$past``, ``$stable``, ``$rose``, and ``$fell``. This functions can
-also be used outside of SVA sequences.
+Any standard Verilog boolean expression is supported, as well as the
+SystemVerilog functions ``$past``, ``$stable``, ``$changed``, ``$rose``, and
+``$fell``. This functions can also be used outside of SVA sequences.
 
 Additionally the ``<sequence>.triggered`` syntax for checking if the end of
-any given sequence matches the current cycle is supported everywhere in expressions
-used in SVA sequences.
+any given sequence matches the current cycle is supported in expressions.
+
+Finally the usual SystemVerilog functions such as ``$countones``, ``$onehot``,
+and ``$onehot0`` are supported, further simplifying writing formal properties.
 
 Sequences
 ~~~~~~~~~
@@ -118,7 +121,7 @@ And *until_condition* is one of:
 Clocking and Reset
 ~~~~~~~~~~~~~~~~~~
 
-The following cunstructs are supported for clocking in reset in most of the
+The following constructs are supported for clocking in reset in most of the
 places the SystemVerilog standard permits them, but properties spanning
 multiple different clock domains are currently not supported.