mirrors/sby
3
0
Fork 0
mirror of https://github.com/YosysHQ/sby.git synced 2025-04-12 16:28:17 +00:00
Code Activity

Update verific.rst

Browse source 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
This commit is contained in:
Clifford Wolf 2018-03-06 11:19:27 +01:00
parent fbd5ddb615
commit f151ea733a
1 changed files with 12 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

21
docs/source/verific.rst
View file

@ -30,10 +30,11 @@ such as
* ``default disable iff`` ... ``;`` * ``default disable iff`` ... ``;``
* ``property`` ... ``endproperty`` * ``property`` ... ``endproperty``
* ``sequence`` ... ``endsequence`` * ``sequence`` ... ``endsequence``
* Parameters to sequences and properties * ``checker`` ... ``endchecker``
* Storing sequences and properties in packages * 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 deep hierarchical references are supported, simplifying the integration of
formal properties with the design under test. formal properties with the design under test.
@ -44,13 +45,15 @@ SystemVerilog formal test-bench into a VHDL design under test.
Expressions in Sequences Expressions in Sequences
~~~~~~~~~~~~~~~~~~~~~~~~ ~~~~~~~~~~~~~~~~~~~~~~~~
Any standard Verilog boolean expression is supported, as well as the SystemVerilog Any standard Verilog boolean expression is supported, as well as the
functions ``$past``, ``$stable``, ``$rose``, and ``$fell``. This functions can SystemVerilog functions ``$past``, ``$stable``, ``$changed``, ``$rose``, and
also be used outside of SVA sequences. ``$fell``. This functions can also be used outside of SVA sequences.
Additionally the ``<sequence>.triggered`` syntax for checking if the end of Additionally the ``<sequence>.triggered`` syntax for checking if the end of
any given sequence matches the current cycle is supported everywhere in expressions any given sequence matches the current cycle is supported in expressions.
used in SVA sequences.
Finally the usual SystemVerilog functions such as ``$countones``, ``$onehot``,
and ``$onehot0`` are supported, further simplifying writing formal properties.
Sequences Sequences
~~~~~~~~~ ~~~~~~~~~
@ -118,7 +121,7 @@ And *until_condition* is one of:
Clocking and Reset 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 places the SystemVerilog standard permits them, but properties spanning
multiple different clock domains are currently not supported. multiple different clock domains are currently not supported.