mirrors/sby
3
0
Fork 0
mirror of https://github.com/YosysHQ/sby.git synced 2025-11-03 22:29:12 +00:00
Code Activity

Add multiclock option

Browse source 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
This commit is contained in:
Clifford Wolf 2018-03-04 14:09:16 +01:00
parent e966f3dca4
commit a94f21abab
2 changed files with 45 additions and 36 deletions
Download patch file Download diff file Expand all files Collapse all files

75
docs/source/reference.rst
View file

@ -27,42 +27,45 @@ Mode Description
All other options have default values and thus are optional. The available All other options have default values and thus are optional. The available
options are: options are:
+-------------+------------+---------------------------------------------------------+ +------------------+------------+---------------------------------------------------------+
| Option | Modes | Description | | Option | Modes | Description |
+=============+============+=========================================================+ +==================+============+=========================================================+
| ``expect`` | All | Expected result as comma-separated list of the tokens | | ``expect`` | All | Expected result as comma-separated list of the tokens |
| | | ``pass``, ``fail``, ``unknown``, ``error``, and | | | | ``pass``, ``fail``, ``unknown``, ``error``, and |
| | | ``timeout``. Unexpected results yield a nonzero return | | | | ``timeout``. Unexpected results yield a nonzero return |
| | | code . Default: ``pass`` | | | | code . Default: ``pass`` |
+-------------+------------+---------------------------------------------------------+ +------------------+------------+---------------------------------------------------------+
| ``timeout`` | All | Timeout in seconds. Default: ``none`` (i.e. no timeout) | | ``timeout`` | All | Timeout in seconds. Default: ``none`` (i.e. no timeout) |
+-------------+------------+---------------------------------------------------------+ +------------------+------------+---------------------------------------------------------+
| ``wait`` | All | Instead of terminating when the first engine returns, | | ``multiclock`` | All | Create a model with multiple clocks and/or asynchronous |
| | | wait for all engines to return and check for | | | | logic. Values: ``on``, ``off``. Default: ``off`` |
| | | consistency. Values: ``on``, ``off``. Default: ``off`` | +------------------+------------+---------------------------------------------------------+
+-------------+------------+---------------------------------------------------------+ | ``wait`` | All | Instead of terminating when the first engine returns, |
| ``aigsmt`` | All | Which SMT2 solver to use for converting AIGER witnesses | | | | wait for all engines to return and check for |
| | | to counter example traces. Use ``none`` to disable | | | | consistency. Values: ``on``, ``off``. Default: ``off`` |
| | | conversion of AIGER witnesses. Default: ``yices`` | +------------------+------------+---------------------------------------------------------+
+-------------+------------+---------------------------------------------------------+ | ``aigsmt`` | All | Which SMT2 solver to use for converting AIGER witnesses |
| ``tbtop`` | All | The top module for generated Verilog test benches, as | | | | to counter example traces. Use ``none`` to disable |
| | | hierarchical path relative to the design top module. | | | | conversion of AIGER witnesses. Default: ``yices`` |
+-------------+------------+---------------------------------------------------------+ +------------------+------------+---------------------------------------------------------+
| ``smtc`` | ``bmc``, | Pass this ``.smtc`` file to the smtbmc engine. All | | ``tbtop`` | All | The top module for generated Verilog test benches, as |
| | ``prove``, | other engines are disabled when this option is used. | | | | hierarchical path relative to the design top module. |
| | ``cover`` | Default: None | +------------------+------------+---------------------------------------------------------+
+-------------+------------+---------------------------------------------------------+ | ``smtc`` | ``bmc``, | Pass this ``.smtc`` file to the smtbmc engine. All |
| ``depth`` | ``bmc``, | Depth of the bounded model check. Only the specified | | | ``prove``, | other engines are disabled when this option is used. |
| | ``cover`` | number of cycles are considered. Default: ``20`` | | | ``cover`` | Default: None |
| +------------+---------------------------------------------------------+ +------------------+------------+---------------------------------------------------------+
| | ``prove`` | Depth for the k-induction performed by the ``smtbmc`` | | ``depth`` | ``bmc``, | Depth of the bounded model check. Only the specified |
| | | engine. Other engines ignore this option in ``prove`` | | | ``cover`` | number of cycles are considered. Default: ``20`` |
| | | mode. Default: ``20`` | | +------------+---------------------------------------------------------+
+-------------+------------+---------------------------------------------------------+ | | ``prove`` | Depth for the k-induction performed by the ``smtbmc`` |
| ``append`` | ``bmc``, | When generating a counter-example trace, add the | | | | engine. Other engines ignore this option in ``prove`` |
| | ``prove``, | specified number of cycles at the end of the trace. | | | | mode. Default: ``20`` |
| | ``cover`` | Default: ``0`` | +------------------+------------+---------------------------------------------------------+
+-------------+------------+---------------------------------------------------------+ | ``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 Engines section
--------------- ---------------

6
sbysrc/sby_core.py
View file

@ -351,6 +351,11 @@ class SbyJob:
print("# running in %s/src/" % self.workdir, file=f) print("# running in %s/src/" % self.workdir, file=f)
for cmd in self.script: for cmd in self.script:
print(cmd, file=f) 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"]: if self.opt_mode in ["bmc", "prove"]:
print("chformal -live -fair -cover -remove", file=f) print("chformal -live -fair -cover -remove", file=f)
if self.opt_mode == "cover": if self.opt_mode == "cover":
@ -463,6 +468,7 @@ class SbyJob:
for s in self.expect: for s in self.expect:
assert s in ["PASS", "FAIL", "UNKNOWN", "ERROR", "TIMEOUT"] assert s in ["PASS", "FAIL", "UNKNOWN", "ERROR", "TIMEOUT"]
self.handle_bool_option("multiclock", False)
self.handle_bool_option("wait", False) self.handle_bool_option("wait", False)
self.handle_int_option("timeout", None) self.handle_int_option("timeout", None)