From e6e57b33e36256f86697950ba6af803225c8b7e3 Mon Sep 17 00:00:00 2001 From: nella Date: Sun, 15 Feb 2026 09:00:04 +0100 Subject: [PATCH 1/4] document abc --keep-going pdr [sc-220]. --- backends/aiger/aiger.cc | 5 +++ .../more_scripting/model_checking.rst | 36 +++++++++++++++++-- passes/cmds/rename.cc | 11 ++++-- 3 files changed, 46 insertions(+), 6 deletions(-) diff --git a/backends/aiger/aiger.cc b/backends/aiger/aiger.cc index 95f4c19e2..62c79f60b 100644 --- a/backends/aiger/aiger.cc +++ b/backends/aiger/aiger.cc @@ -931,6 +931,11 @@ struct AigerBackend : public Backend { log("\n"); log(" -ywmap \n"); log(" write a map file for conversion to and from yosys witness traces.\n"); + log(" The generated JSON map includes \"asserts\" and \"assumes\" arrays\n"); + log(" containing the hierarchical witness paths of the corresponding\n"); + log(" $assert and $assume cells. This enables downstream tools to map\n"); + log(" AIGER bad-state properties and invariant constraints back to\n"); + log(" individual formal properties by name.\n"); log("\n"); log(" -I, -O, -B, -L\n"); log(" If the design contains no input/output/assert/flip-flop then create one\n"); diff --git a/docs/source/using_yosys/more_scripting/model_checking.rst b/docs/source/using_yosys/more_scripting/model_checking.rst index 799c99b6f..da9193a6f 100644 --- a/docs/source/using_yosys/more_scripting/model_checking.rst +++ b/docs/source/using_yosys/more_scripting/model_checking.rst @@ -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. diff --git a/passes/cmds/rename.cc b/passes/cmds/rename.cc index 078ffb769..f87396743 100644 --- a/passes/cmds/rename.cc +++ b/passes/cmds/rename.cc @@ -263,9 +263,14 @@ struct RenamePass : public Pass { log(" rename -witness\n"); log("\n"); log("Assigns auto-generated names to all $any*/$all* output wires and containing\n"); - log("cells that do not have a public name. This ensures that, during formal\n"); - log("verification, a solver-found trace can be fully specified using a public\n"); - log("hierarchical names.\n"); + log("cells that do not have a public name. Also renames formal property cells\n"); + log("($assert, $assume, $cover, $live, $fair, $check) that have private names,\n"); + log("giving them public witness-trackable names.\n"); + log("\n"); + log("This ensures that, during formal verification, a solver-found trace can be\n"); + log("fully specified using public hierarchical names, and that individual property\n"); + log("results can be tracked by name in flows that support per-property reporting\n"); + log("(e.g. SBY with abc pdr in --keep-going mode).\n"); log("\n"); log("\n"); log(" rename -hide [selection]\n"); From 2b4f481850d7ddc160e34d68e201917e508e25c7 Mon Sep 17 00:00:00 2001 From: nella Date: Wed, 18 Feb 2026 09:24:41 +0100 Subject: [PATCH 2/4] Cleanup docs. --- backends/aiger/aiger.cc | 9 +++---- .../more_scripting/model_checking.rst | 24 +++++++++---------- passes/cmds/rename.cc | 13 ++++------ 3 files changed, 19 insertions(+), 27 deletions(-) diff --git a/backends/aiger/aiger.cc b/backends/aiger/aiger.cc index 62c79f60b..0c49e84b8 100644 --- a/backends/aiger/aiger.cc +++ b/backends/aiger/aiger.cc @@ -930,12 +930,9 @@ struct AigerBackend : public Backend { log(" make indexes zero based, enable using map files with smt solvers.\n"); log("\n"); log(" -ywmap \n"); - log(" write a map file for conversion to and from yosys witness traces.\n"); - log(" The generated JSON map includes \"asserts\" and \"assumes\" arrays\n"); - log(" containing the hierarchical witness paths of the corresponding\n"); - log(" $assert and $assume cells. This enables downstream tools to map\n"); - log(" AIGER bad-state properties and invariant constraints back to\n"); - log(" individual formal properties by name.\n"); + log(" write a map file for conversion to and from yosys witness traces,\n"); + log(" also allows for mapping AIGER bad-state properties and invariant\n"); + log(" constraints back to individual formal properties by name.\n"); log("\n"); log(" -I, -O, -B, -L\n"); log(" If the design contains no input/output/assert/flip-flop then create one\n"); diff --git a/docs/source/using_yosys/more_scripting/model_checking.rst b/docs/source/using_yosys/more_scripting/model_checking.rst index da9193a6f..b418f6aff 100644 --- a/docs/source/using_yosys/more_scripting/model_checking.rst +++ b/docs/source/using_yosys/more_scripting/model_checking.rst @@ -121,29 +121,29 @@ 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 -SymbiYosys), Yosys provides infrastructure for tracking individual formal +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 +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`` +- 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 +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 +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). +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 +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. diff --git a/passes/cmds/rename.cc b/passes/cmds/rename.cc index f87396743..836dfe5b1 100644 --- a/passes/cmds/rename.cc +++ b/passes/cmds/rename.cc @@ -262,15 +262,10 @@ struct RenamePass : public Pass { log("\n"); log(" rename -witness\n"); log("\n"); - log("Assigns auto-generated names to all $any*/$all* output wires and containing\n"); - log("cells that do not have a public name. Also renames formal property cells\n"); - log("($assert, $assume, $cover, $live, $fair, $check) that have private names,\n"); - log("giving them public witness-trackable names.\n"); - log("\n"); - log("This ensures that, during formal verification, a solver-found trace can be\n"); - log("fully specified using public hierarchical names, and that individual property\n"); - log("results can be tracked by name in flows that support per-property reporting\n"); - log("(e.g. SBY with abc pdr in --keep-going mode).\n"); + log("Assigns auto-generated names to objects used in formal verification\n"); + log("that do not have a public name. This applies to all formal property\n"); + log("cells ($assert, $assume, $cover, $live, $fair, $check), $any*/$all*\n"); + log("output wires, and their containing cells.\n"); log("\n"); log("\n"); log(" rename -hide [selection]\n"); From 01e89a8f9e8ea16d2bab74f725c19d6348fc5f46 Mon Sep 17 00:00:00 2001 From: nella Date: Wed, 18 Feb 2026 09:29:35 +0100 Subject: [PATCH 3/4] Remove cell mentions. --- .../more_scripting/model_checking.rst | 17 ++++++++--------- passes/cmds/rename.cc | 7 +++---- 2 files changed, 11 insertions(+), 13 deletions(-) diff --git a/docs/source/using_yosys/more_scripting/model_checking.rst b/docs/source/using_yosys/more_scripting/model_checking.rst index b418f6aff..02400d5d8 100644 --- a/docs/source/using_yosys/more_scripting/model_checking.rst +++ b/docs/source/using_yosys/more_scripting/model_checking.rst @@ -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. diff --git a/passes/cmds/rename.cc b/passes/cmds/rename.cc index 836dfe5b1..a07d588c4 100644 --- a/passes/cmds/rename.cc +++ b/passes/cmds/rename.cc @@ -254,10 +254,9 @@ struct RenamePass : public Pass { log("\n"); log(" rename -enumerate [-pattern ] [selection]\n"); log("\n"); - log("Assign short auto-generated names to all selected wires and cells with private\n"); - log("names. The -pattern option can be used to set the pattern for the new names.\n"); - log("The character %% in the pattern is replaced with a integer number. The default\n"); - log("pattern is '_%%_'.\n"); + log("Assigns auto-generated names to objects used in formal verification\n"); + log("that do not have a public name. This applies to all formal property\n"); + log("cells, $any*/$all* output wires, and their containing cells.\n"); log("\n"); log("\n"); log(" rename -witness\n"); From 2c52546e2a9b1ac94c1ddfdd88ef80238c412c7e Mon Sep 17 00:00:00 2001 From: nella Date: Wed, 25 Feb 2026 16:42:05 +0100 Subject: [PATCH 4/4] 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