mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2026-03-02 03:36:56 +00:00
Code Activity

Remove cell mentions.

Browse source
This commit is contained in:
nella 2026-02-18 09:29:35 +01:00
parent 2b4f481850
commit 01e89a8f9e
2 changed files with 11 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -136,14 +136,13 @@ names to all cells that participate in the witness framework:
These public names allow downstream tools to refer to individual properties by
their hierarchical path rather than by anonymous internal identifiers.
The `write_aiger -ywmap` option generates a JSON map file that includes, among
other things, ``"asserts"`` and ``"assumes"`` arrays. Each entry contains the
hierarchical witness path of the corresponding `$assert` or `$assume` cell.
This lets tools such as SBY map AIGER bad-state properties and invariant
constraints back to individual formal properties, enabling features like
per-property pass/fail reporting (e.g. `abc pdr` with ``--keep-going`` mode).
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
``--keep-going`` mode).
The `write_smt2` backend similarly uses the public witness names when emitting
``yosys-smt2-assert`` and ``yosys-smt2-assume`` comments. Cells whose
``hdlname`` attribute contains the ``_witness_`` marker are treated as having
private names for comment purposes, keeping solver output clean.
SMT2 comments. Cells whose ``hdlname`` attribute contains the ``_witness_``
marker are treated as having private names for comment purposes, keeping solver
output clean.