From f151ea733a93bada9f9d3012c7d43a6dc45fc704 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Tue, 6 Mar 2018 11:19:27 +0100 Subject: [PATCH] Update verific.rst Signed-off-by: Clifford Wolf --- docs/source/verific.rst | 21 ++++++++++++--------- 1 file changed, 12 insertions(+), 9 deletions(-) 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 ``.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. -- 2.30.2