riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity
yosys/docs/source/cell/word_formal.rst

32 lines
710 B
ReStructuredText
Raw Normal View History

cellref: Deprecate cell_library.rst Most of the word/coarse level cells have an assigned group and individual page. The gate/fine level cells are all on one page. Fix links to `cell_library.rst`.
2024-05-26 22:46:43 -05:00
Formal verification cells
-------------------------
Docs: Add note on $check
2024-09-15 20:02:54 -05:00
.. role:: yoscrypt(code)
:language: yoscrypt
Docs: Add todo for $check
2024-08-28 17:43:46 -05:00
Docs: Add note on $check
2024-09-15 20:02:54 -05:00
.. note::
Some front-ends may not support the generic `$check` cell, in such cases
calling :yoscrypt:`chformal -lower` will convert each `$check` cell into it's
equivalent. See `chformal` for more.
Docs: Add todo for $check
2024-08-28 17:43:46 -05:00
Docs: TODOs block, todos don't
2024-09-04 23:22:16 -05:00
.. todo:: Describe formal cells
cellref: Deprecate cell_library.rst Most of the word/coarse level cells have an assigned group and individual page. The gate/fine level cells are all on one page. Fix links to `cell_library.rst`.
2024-05-26 22:46:43 -05:00
`$check`, `$assert`, `$assume`, `$live`, `$fair`, `$cover`, `$equiv`,
`$initstate`, `$anyconst`, `$anyseq`, `$anyinit`, `$allconst`, and `$allseq`.
Also `$ff` and `$_FF_` cells.
.. autocellgroup:: formal
:members:
:source:
:linenos:
Docs: Assign remaining word cells to groups Move todos to correct place. Add todo for x-prop cells.
2024-08-26 17:48:28 -05:00
Formal support cells
~~~~~~~~~~~~~~~~~~~~
.. autocellgroup:: formal_tag
:members:
:source:
:linenos: