docs/source/verific.rst

   1
   2 SystemVerilog, VHDL, SVA
   3 ========================
   4
   5 TBD
   6
   7 ``verific -sv <files>``
   8
   9 ``verific -vhdl <files>``
  10
  11 ``verific -import <top>``
  12
  13 TBD
  14
  15 Supported SVA Property Syntax
  16 -----------------------------
  17
  18 SVA support in Yosys' Verific bindings is currently in development. At the time
  19 of writing, the following subset of SVA property syntax is supported in
  20 concurrent assertions, assumptions, and cover statements when using the
  21 ``verific`` command in Yosys to read the design.
  22
  23 High-Level Convenience Features
  24 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  25
  26 Most of the high-level convenience features of the SVA language are supported,
  27 such as
  28
  29   * ``default clocking`` ... ``endclocking``
  30   * ``default disable iff`` ... ``;``
  31   * ``property`` ... ``endproperty``
  32   * ``sequence`` ... ``endsequence``
  33   * ``checker`` ... ``endchecker``
  34   * Arguments to sequences, properties, and checkers
  35   * Storing sequences, properties, and checkers in packages
  36
  37 In addition the SVA-specific features, the SystemVerilog ``bind`` statement and
  38 deep hierarchical references are supported, simplifying the integration of
  39 formal properties with the design under test.
  40
  41 The ``verific`` command also allows parsing of VHDL designs and supports binding
  42 SystemVerilog modules to VHDL entities and deep hierarchical references from a
  43 SystemVerilog formal test-bench into a VHDL design under test.
  44
  45 Expressions in Sequences
  46 ~~~~~~~~~~~~~~~~~~~~~~~~
  47
  48 Any standard Verilog boolean expression is supported, as well as the
  49 SystemVerilog functions ``$past``, ``$stable``, ``$changed``, ``$rose``, and
  50 ``$fell``. This functions can also be used outside of SVA sequences.
  51
  52 Additionally the ``<sequence>.triggered`` syntax for checking if the end of
  53 any given sequence matches the current cycle is supported in expressions.
  54
  55 Finally the usual SystemVerilog functions such as ``$countones``, ``$onehot``,
  56 and ``$onehot0`` are also supported.
  57
  58 Sequences
  59 ~~~~~~~~~
  60
  61 Most importantly, expressions and variable-length concatenation are supported:
  62
  63   * *expression*
  64   * *sequence* ``##N`` *sequence*
  65   * *sequence* ``##[*]`` *sequence*
  66   * *sequence* ``##[+]`` *sequence*
  67   * *sequence* ``##[N:M]`` *sequence*
  68   * *sequence* ``##[N:$]`` *sequence*
  69
  70 Also variable-length repetition:
  71
  72   * *sequence* ``[*]``
  73   * *sequence* ``[+]``
  74   * *sequence* ``[*N]``
  75   * *sequence* ``[*N:M]``
  76   * *sequence* ``[*N:$]``
  77
  78 And the following more complex operators:
  79
  80   * *sequence* ``or`` *sequence*
  81   * *sequence* ``and`` *sequence*
  82   * *expression* ``throughout`` *sequence*
  83   * *sequence* ``intersect`` *sequence*
  84   * *sequence* ``within`` *sequence*
  85   * ``first_match(`` *sequence* ``)``
  86   * *expression* ``[=N]``
  87   * *expression* ``[=N:M]``
  88   * *expression* ``[=N:$]``
  89   * *expression* ``[->N]``
  90   * *expression* ``[->N:M]``
  91   * *expression* ``[->N:$]``
  92
  93 Properties
  94 ~~~~~~~~~~
  95
  96 Currently only a certain set of patterns are supported for SVA properties:
  97
  98   * [*antecedent_condition*] *sequence*
  99   * [*antecedent_condition*] ``not`` *sequence*
 100   * *antecedent_condition* *sequence* *until_condition*
 101   * *antecedent_condition* ``not`` *sequence* *until_condition*
 102
 103 Where *antecedent_condition* is one of:
 104
 105   * sequence ``|->``
 106   * sequence ``|=>``
 107
 108 And *until_condition* is one of:
 109
 110   * ``until`` *expression*
 111   * ``s_until`` *expression*
 112   * ``until_with`` *expression*
 113   * ``s_until_with`` *expression*
 114
 115 Clocking and Reset
 116 ~~~~~~~~~~~~~~~~~~
 117
 118 The following constructs are supported for clocking and reset in most of the
 119 places the SystemVerilog standard permits them. However, properties spanning
 120 multiple different clock domains are currently unsupported.
 121
 122   * ``@(posedge`` *clock* ``)``
 123   * ``@(negedge`` *clock* ``)``
 124   * ``@(posedge`` *clock* ``iff`` *enable* ``)``
 125   * ``@(negedge`` *clock* ``iff`` *enable* ``)``
 126   * ``disable iff (`` *expression* ``)``
 127