From: ZipCPU Date: Wed, 22 May 2019 00:55:46 +0000 (-0400) Subject: Updated Verilog documentation X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2462855e0fed6b43666df07f5e94e224c74d2efb;p=SymbiYosys.git Updated Verilog documentation --- diff --git a/docs/source/verilog.rst b/docs/source/verilog.rst index d83b299..f43f71f 100644 --- a/docs/source/verilog.rst +++ b/docs/source/verilog.rst @@ -2,33 +2,152 @@ Formal extensions to Verilog ============================ -TBD +Any Verilog file may be read using ``read -formal `` within the +SymbiYosys ``script`` section. Multiple files may be given on the sames +line, or various files may be read in subsequent lines. + +``read -formal`` will also define the ``FORMAL`` macro, which can be used +to separate a section having formal properties from the rest of the logic +within the core. + +.. code-block:: systemverilog -``read -sv`` + module somemodule(port1, port2, ...); + // User logic here + // + `ifdef FORMAL + // Formal properties here + `endif + endmodule -``read_verilog -sv`` +The ``bind()`` operator can also be used when using the Verific front end. +This will provide an option to attach formal properties to a given piece +of logic, without actually modifying the module in question to do so as +we did in the example above. SystemVerilog Immediate Assertions ---------------------------------- -TBD +SymbiYosys supports three basic immediate assertion types. + +1. ``assume();`` + + An assumption restricts the possibilities the formal tool examines, making + the search space smaller. In any solver generated trace, all of the + assumptions will always be true. + +2. ``assert();`` + + An assertion is something the solver will try to make false. Any time + SymbiYosys is run with ``mode bmc``, the proof will fail if some set + of inputs can cause the ```` within the assertion to be zero (false). + When SymbiYosys is run with ``mode prove``, the proof may also yield an + ``UNKNOWN`` result if an assertion can be made to fail during the induction + step. + +3. ``cover();`` + + A cover statement only applies when SymbiYosys is ran with option + ``mode cover``. In this case, the formal solver will start at the + beginning of time (i.e. when all initial statements are true), and it will + try to find some clock when ```` can be made to be true. Such a + cover run will "PASS" once all internal ``cover()`` statements have been + fulfilled. It will "FAIL" if any ``cover()`` statement exists that cannot + be reached in the first ``N`` states, where ``N`` is set by the + ``depth`` option. A cover pass will also fail if an assertion needs to + be broken in order to reach the covered state. + +To be used, each of these statements needs to be placed into an *immediate* +context. That is, it needs to be placed within an ``always`` block of some +type. Two types of ``always`` block contexts are permitted: + +- ``always @(*)`` + + Formal properties within an ``always @(*)`` block will be checked on every + time step. For synchronous proofs, the property will be checked every + clock period. For asynchronous proofs, i.e. those with ``multiclock on``, + the property will still be checked on every time step but, depending upon + how you set up your time steps, it may also be checked multiple times + per clock interval. + + As an example, consider the following assertion that the ``error_flag`` + signal must remain low. + +.. code-block:: systemverilog + + always @(*) + assert(!error_flag); + +While it is not recommended that formal properties be mixed with logic in +the same ``always @(*)`` block, the language supports it. In such cases, +the formal property will be evaluated as though it took place in the middle +of the logic block. + +- ``always @(posedge )`` + + The second form of immediate assertion is one within a clocked always block. + This form of assertion is required when attempting to use the ``$past``, + ``$stable``, ``$changed``, ``$rose``, or ``$fell`` SystemVerilog functions + discussed in the next section. -``assert();`` + Unlike the ``@(*)`` assertion, this one will only be checked on the clock + edge. Depending upon how the clock is set up, that may mean that there are + several formal time steps between when this assertion is checked. -``assume();`` + The two types of immediate assertions, both with and without a clock + reference, are very similar. There is one critical difference between + them, however. The clocked assertion will not be checked until the + positive edge of the clock following the time period in question. Within + a synchronous design, this means that the fault will not lie on the last + time step, but rather the time step prior. New users often find this + non-intuitive. -``cover();`` +One subtlety to be aware of is that any ``always @(*)`` assertion that +depends upon an ``always @(posedge )`` assumption might fail before +the assumption is applied. One solution is to use all clocked or all +combinatorial blocks. Another solution is to move the assertion into an +``always @(posedge )`` block. SystemVerilog Functions ----------------------- -TBD +Yosys supports five formal related functions: ``$past``, ``$stable``, +``$changed``, ``$rose``, and ``$fell``. Internally, these are all implemented +in terms of the implementation of the ``$past`` operator. + +The ``$past()`` function returns the value of ```` from one clock +ago. It can only be used within a clocked always block, since the clock is +used to define "one clock ago." It is roughly equivalent to, + +.. code-block:: systemverilog + + reg past_value; + always @(posedge clock) + past_value <= expression; + +There are two keys to the use of ``$past``. The first is that +``$past()`` can only be used within a clocked always block. The second +is that there is no initial value given to any ``$past()``. That means +that on the first clock period of any design, ``$past()`` will be +undefined. -``$past`` +Yosys supports both one and two arguments to ``$past``. In the two argument +form, ``$past(,N)``, the expression returns the value of ```` +from ``N`` clocks ago. ``N`` must be a synthesis time constant. -``$stable`` +``$stable()`` is short hand for `` == $past()``. -``$rose``, ``$fell`` +``$changed()`` is short hand for `` != $past()``. + +While the next two functions, ``$rose`` and ``$fell``, can be applied to +multi-bit expressions, only the least significant bits will be examined. +If we allow that ```` has only a single bit within it, perhaps selected +from the least significant bit of a larger expression, then we can +express the following equivalencies. + +``$rose()`` is short hand for `` && !$past()`` is short hand for ``! && $past(