From: Clifford Wolf <clifford@clifford.at>
Date: Tue, 6 Mar 2018 22:46:52 +0000 (+0100)
Subject: Update verific.rst
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=055b305c81ffafeb97818e9b2b0c94444896b3de;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 2d5f868..4ea9c67 100644
--- a/docs/source/verific.rst
+++ b/docs/source/verific.rst
@@ -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* ``)``