From 2c52546e2a9b1ac94c1ddfdd88ef80238c412c7e Mon Sep 17 00:00:00 2001 From: nella Date: Wed, 25 Feb 2026 16:42:05 +0100 Subject: [PATCH] Fix docs. --- docs/source/using_yosys/more_scripting/model_checking.rst | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/docs/source/using_yosys/more_scripting/model_checking.rst b/docs/source/using_yosys/more_scripting/model_checking.rst index 02400d5d8..cbf5dc7b0 100644 --- a/docs/source/using_yosys/more_scripting/model_checking.rst +++ b/docs/source/using_yosys/more_scripting/model_checking.rst @@ -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