From a94f21abab5b11fc24cff2ffd7490b54b3d9f241 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Sun, 4 Mar 2018 14:09:16 +0100 Subject: [PATCH] Add multiclock option Signed-off-by: Clifford Wolf --- docs/source/reference.rst | 75 ++++++++++++++++++++------------------- sbysrc/sby_core.py | 6 ++++ 2 files changed, 45 insertions(+), 36 deletions(-) diff --git a/docs/source/reference.rst b/docs/source/reference.rst index ca8075a..1ac0753 100644 --- a/docs/source/reference.rst +++ b/docs/source/reference.rst @@ -27,42 +27,45 @@ Mode Description All other options have default values and thus are optional. The available options are: -+-------------+------------+---------------------------------------------------------+ -| Option | Modes | Description | -+=============+============+=========================================================+ -| ``expect`` | All | Expected result as comma-separated list of the tokens | -| | | ``pass``, ``fail``, ``unknown``, ``error``, and | -| | | ``timeout``. Unexpected results yield a nonzero return | -| | | code . Default: ``pass`` | -+-------------+------------+---------------------------------------------------------+ -| ``timeout`` | All | Timeout in seconds. Default: ``none`` (i.e. no timeout) | -+-------------+------------+---------------------------------------------------------+ -| ``wait`` | All | Instead of terminating when the first engine returns, | -| | | wait for all engines to return and check for | -| | | consistency. Values: ``on``, ``off``. Default: ``off`` | -+-------------+------------+---------------------------------------------------------+ -| ``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`` | -+-------------+------------+---------------------------------------------------------+ -| ``tbtop`` | All | The top module for generated Verilog test benches, as | -| | | hierarchical path relative to the design top module. | -+-------------+------------+---------------------------------------------------------+ -| ``smtc`` | ``bmc``, | Pass this ``.smtc`` file to the smtbmc engine. All | -| | ``prove``, | other engines are disabled when this option is used. | -| | ``cover`` | Default: None | -+-------------+------------+---------------------------------------------------------+ -| ``depth`` | ``bmc``, | Depth of the bounded model check. Only the specified | -| | ``cover`` | number of cycles are considered. Default: ``20`` | -| +------------+---------------------------------------------------------+ -| | ``prove`` | Depth for the k-induction performed by the ``smtbmc`` | -| | | engine. Other engines ignore this option in ``prove`` | -| | | mode. Default: ``20`` | -+-------------+------------+---------------------------------------------------------+ -| ``append`` | ``bmc``, | When generating a counter-example trace, add the | -| | ``prove``, | specified number of cycles at the end of the trace. | -| | ``cover`` | Default: ``0`` | -+-------------+------------+---------------------------------------------------------+ ++------------------+------------+---------------------------------------------------------+ +| Option | Modes | Description | ++==================+============+=========================================================+ +| ``expect`` | All | Expected result as comma-separated list of the tokens | +| | | ``pass``, ``fail``, ``unknown``, ``error``, and | +| | | ``timeout``. Unexpected results yield a nonzero return | +| | | code . Default: ``pass`` | ++------------------+------------+---------------------------------------------------------+ +| ``timeout`` | All | Timeout in seconds. Default: ``none`` (i.e. no timeout) | ++------------------+------------+---------------------------------------------------------+ +| ``multiclock`` | All | Create a model with multiple clocks and/or asynchronous | +| | | logic. Values: ``on``, ``off``. Default: ``off`` | ++------------------+------------+---------------------------------------------------------+ +| ``wait`` | All | Instead of terminating when the first engine returns, | +| | | wait for all engines to return and check for | +| | | consistency. Values: ``on``, ``off``. Default: ``off`` | ++------------------+------------+---------------------------------------------------------+ +| ``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`` | ++------------------+------------+---------------------------------------------------------+ +| ``tbtop`` | All | The top module for generated Verilog test benches, as | +| | | hierarchical path relative to the design top module. | ++------------------+------------+---------------------------------------------------------+ +| ``smtc`` | ``bmc``, | Pass this ``.smtc`` file to the smtbmc engine. All | +| | ``prove``, | other engines are disabled when this option is used. | +| | ``cover`` | Default: None | ++------------------+------------+---------------------------------------------------------+ +| ``depth`` | ``bmc``, | Depth of the bounded model check. Only the specified | +| | ``cover`` | number of cycles are considered. Default: ``20`` | +| +------------+---------------------------------------------------------+ +| | ``prove`` | Depth for the k-induction performed by the ``smtbmc`` | +| | | engine. Other engines ignore this option in ``prove`` | +| | | mode. Default: ``20`` | ++------------------+------------+---------------------------------------------------------+ +| ``append`` | ``bmc``, | When generating a counter-example trace, add the | +| | ``prove``, | specified number of cycles at the end of the trace. | +| | ``cover`` | Default: ``0`` | ++------------------+------------+---------------------------------------------------------+ Engines section --------------- diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py index cbb7e07..95d11a1 100644 --- a/sbysrc/sby_core.py +++ b/sbysrc/sby_core.py @@ -351,6 +351,11 @@ class SbyJob: print("# running in %s/src/" % self.workdir, file=f) for cmd in self.script: print(cmd, file=f) + if self.opt_multiclock: + print("clk2fflogic", file=f) + else: + print("techmap -map +/adff2dff.v", file=f) + print("chformal -assume -early", file=f) if self.opt_mode in ["bmc", "prove"]: print("chformal -live -fair -cover -remove", file=f) if self.opt_mode == "cover": @@ -463,6 +468,7 @@ class SbyJob: for s in self.expect: assert s in ["PASS", "FAIL", "UNKNOWN", "ERROR", "TIMEOUT"] + self.handle_bool_option("multiclock", False) self.handle_bool_option("wait", False) self.handle_int_option("timeout", None) -- 2.30.2