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

document abc --keep-going pdr [sc-220].

Browse source
This commit is contained in:
nella 2026-02-15 09:00:04 +01:00
parent a6e33d9916
commit e6e57b33e3
3 changed files with 46 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -3,9 +3,9 @@ Symbolic model checking
.. todo:: check text context
.. note::
While it is possible to perform model checking directly in Yosys, it
.. note::
While it is possible to perform model checking directly in Yosys, it
is highly recommended to use SBY or EQY for formal hardware verification.
Symbolic Model Checking (SMC) is used to formally prove that a circuit has (or
@ -117,3 +117,33 @@ Result with fixed :file:`axis_master.v`:
Solving problem with 159144 variables and 441626 clauses..
SAT proof finished - no model found: SUCCESS!
Witness framework and per-property tracking
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When using AIGER-based formal verification flows (such as the ``abc`` engine in
SymbiYosys), 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:
- Witness signal cells: ``$anyconst``, ``$anyseq``, ``$anyinit``,
``$allconst``, ``$allseq``
- Formal property cells: ``$assert``, ``$assume``, ``$cover``, ``$live``,
``$fair``, ``$check``
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 SymbiYosys 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_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.