mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2026-03-01 11:16:55 +00:00
Code Activity

Fix docs.

Browse source
This commit is contained in:
nella 2026-02-25 16:42:05 +01:00
parent 01e89a8f9e
commit 2c52546e2a
1 changed files with 4 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

8
docs/source/using_yosys/more_scripting/model_checking.rst
View file

@ -121,12 +121,12 @@ Result with fixed :file:`axis_master.v`:
Witness framework and per-property tracking
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When using AIGER-based formal verification flows (such as the `abc` engine in
When using AIGER-based formal verification flows (such as the ``abc`` engine in
SBY), Yosys provides infrastructure for tracking individual formal
properties through the verification pipeline.
The `rename -witness` pass (run automatically by `prep`) assigns public
names to all cells that participate in the witness framework:
The `rename -witness` pass assigns public names to all cells that participate in
the witness framework:
- Witness signal cells: `$anyconst`, `$anyseq`, `$anyinit`,
`$allconst`, `$allseq`
@ -139,7 +139,7 @@ their hierarchical path rather than by anonymous internal identifiers.
The `write_aiger -ywmap` option generates a map file for conversion to and from
Yosys witness traces, and also allows for mapping AIGER bad-state properties and
invariant constraints back to individual formal properties by name. This enables
features like per-property pass/fail reporting (e.g. `abc pdr` with
features like per-property pass/fail reporting (e.g. ``abc pdr`` with
``--keep-going`` mode).
The `write_smt2` backend similarly uses the public witness names when emitting