From 6d0a1ed960491fb68fec11d71f5946f35a1a8418 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Mon, 20 Oct 2025 14:57:38 +0200 Subject: [PATCH] Add `cycle_width` option for sim's new `-width` option --- docs/source/reference.rst | 3 +++ sbysrc/sby_core.py | 3 +++ sbysrc/sby_sim.py | 2 ++ 3 files changed, 8 insertions(+) diff --git a/docs/source/reference.rst b/docs/source/reference.rst index 3f0a739..14bdb54 100644 --- a/docs/source/reference.rst +++ b/docs/source/reference.rst @@ -160,6 +160,9 @@ options are: | ``fst`` | All | Generate FST traces using Yosys's sim command. | | | | Values: ``on``, ``off``. Default: ``off`` | +-------------------+------------+---------------------------------------------------------+ +| ``cycle_width`` | All | Cycle width used by Yosys's sim command. | +| | | Values: even numbers >= 2. Default: ``10`` | ++-------------------+------------+---------------------------------------------------------+ | ``aigsmt`` | All | Which SMT2 solver to use for converting AIGER witnesses | | | | to counter example traces. Use ``none`` to disable | | | | conversion of AIGER witnesses. Default: ``yices`` | diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py index 17b1ae9..7a67cd3 100644 --- a/sbysrc/sby_core.py +++ b/sbysrc/sby_core.py @@ -1395,6 +1395,9 @@ class SbyTask(SbyConfig): self.handle_bool_option("vcd", True) self.handle_bool_option("vcd_sim", False) self.handle_bool_option("fst", False) + self.handle_int_option("cycle_width", 10) + if self.opt_cycle_width < 2 or self.opt_cycle_width % 2 != 0: + self.error(f"cycle_width option must be an even number >= 2, but is {self.opt_cycle_width}") self.handle_bool_option("witrename", True) self.handle_bool_option("aigfolds", False) diff --git a/sbysrc/sby_sim.py b/sbysrc/sby_sim.py index 4658407..32789fb 100644 --- a/sbysrc/sby_sim.py +++ b/sbysrc/sby_sim.py @@ -44,6 +44,8 @@ def sim_witness_trace(prefix, task, engine_idx, witness_file, *, append, inducti sim_args = "" if inductive: sim_args += " -noinitstate" + if task.opt_cycle_width != 10: + formats.append(f"-width {task.opt_cycle_width}") print(f"sim -hdlname -summary {trace_name}.json -append {append}{sim_args} -r {trace_name}.yw {' '.join(formats)}", file=f) def exit_callback(retval):