Update verific.rst
authorClifford Wolf <clifford@clifford.at>
Tue, 6 Mar 2018 22:46:52 +0000 (23:46 +0100)
committerClifford Wolf <clifford@clifford.at>
Tue, 6 Mar 2018 22:46:52 +0000 (23:46 +0100)
Signed-off-by: Clifford Wolf <clifford@clifford.at>
docs/source/verific.rst

index 2d5f868cad355e804bb627ed26311358441b14be..4ea9c6768ac4961e56fa8520c05b692ba3aa372c 100644 (file)
@@ -53,15 +53,11 @@ Additionally the ``<sequence>.triggered`` syntax for checking if the end of
 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.
+and ``$onehot0`` are also supported.
 
 Sequences
 ~~~~~~~~~
 
-The following sequence operators are currently supported. Note that some of
-them only allow expressions in places where complete SVA would allow sequences
-as well.
-
 Most importantly, expressions and variable-length concatenation are supported:
 
   * *expression*
@@ -73,13 +69,13 @@ Most importantly, expressions and variable-length concatenation are supported:
 
 Also variable-length repetition:
 
-  * *expression* ``[*]``
-  * *expression* ``[+]``
-  * *expression* ``[*N]``
-  * *expression* ``[*N:M]``
-  * *expression* ``[*N:$]``
+  * *sequence* ``[*]``
+  * *sequence* ``[+]``
+  * *sequence* ``[*N]``
+  * *sequence* ``[*N:M]``
+  * *sequence* ``[*N:$]``
 
-And some additional more complex operators:
+And the following more complex operators:
 
   * *sequence* ``or`` *sequence*
   * *sequence* ``and`` *sequence*
@@ -119,9 +115,9 @@ And *until_condition* is one of:
 Clocking and Reset
 ~~~~~~~~~~~~~~~~~~
 
-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.
+The following constructs are supported for clocking and reset in most of the
+places the SystemVerilog standard permits them. However, properties spanning
+multiple different clock domains are currently unsupported.
 
   * ``@(posedge`` *clock* ``)``
   * ``@(negedge`` *clock* ``)``