Add multiclock option

Signed-off-by: Clifford Wolf <clifford@clifford.at>

diff --git a/docs/source/reference.rst b/docs/source/reference.rst
index ca8075a955a7ac28954e19824c3c4d3b138b2538..1ac07532a88e3766c24924320f3a60bc767cb988 100644 (file)
--- 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 cbb7e07fc5390805447ef3aad678f687e8f0c562..95d11a1662b8e9857d63191c2f30b5ef7df8fd16 100644 (file)
--- 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)