Add "cover" mode

diff --git a/docs/examples/quickstart/.gitignore b/docs/examples/quickstart/.gitignore
index b0c09d4d491c8f91dedd40d14718cab0f1de8bc3..b157dcfe02cc47cbb768ff2ad17c81dfcfd5e59a 100644 (file)
--- a/docs/examples/quickstart/.gitignore
+++ b/docs/examples/quickstart/.gitignore
@@ -1,3 +1,4 @@
 demo
 memory
 prove
+cover

diff --git a/docs/examples/quickstart/cover.sby b/docs/examples/quickstart/cover.sby
new file mode 100644 (file)
index 0000000..58cce3a
--- /dev/null
+++ b/docs/examples/quickstart/cover.sby
@@ -0,0 +1,12 @@
+[options]
+mode cover
+
+[engines]
+smtbmc
+
+[script]
+read_verilog -formal cover.v
+prep -top top
+
+[files]
+cover.v

diff --git a/docs/examples/quickstart/cover.v b/docs/examples/quickstart/cover.v
new file mode 100644 (file)
index 0000000..4b0d475
--- /dev/null
+++ b/docs/examples/quickstart/cover.v
@@ -0,0 +1,13 @@
+module top (
+       input clk,
+       input [7:0] din
+);
+       reg [31:0] state = 0;
+
+       always @(posedge clk) begin
+               state <= ((state << 5) + state) ^ din;
+       end
+
+       cover property (state == 'd 12345678);
+       cover property (state == 'h 12345678);
+endmodule

diff --git a/docs/source/index.rst b/docs/source/index.rst
index daf29ba37e8948875cab7b4363cf880f6d33c3db..fb5489c2434279e03f22fd38bacdb874c91f441b 100644 (file)
--- a/docs/source/index.rst
+++ b/docs/source/index.rst
@@ -8,7 +8,7 @@ formal tasks:
 
    * Bounded verification of safety properties (assertions)
    * Unbounded verification of safety properties
-   * Generation of test benches from cover statements [TBD]
+   * Generation of test benches from cover statements
    * Verification of liveness properties [TBD]
    * Formal equivalence checking [TBD]
 

diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py
index 5c5313933a58c85eb93563f73d07a3d3e77817ef..3adc6a9568df05ec4523a29239af1a356693a629 100644 (file)
--- a/sbysrc/sby_core.py
+++ b/sbysrc/sby_core.py
@@ -340,6 +340,10 @@ class SbyJob:
             import sby_mode_prove
             sby_mode_prove.run(self)
 
+        elif self.options["mode"] == "cover":
+            import sby_mode_cover
+            sby_mode_cover.run(self)
+
         else:
             assert False
 

diff --git a/sbysrc/sby_engine_smtbmc.py b/sbysrc/sby_engine_smtbmc.py
index f717beec4aa2bd041738578da988de1393a2d650..c57bf476e9daac83f3c79a398b1a249f78e585ad 100644 (file)
--- a/sbysrc/sby_engine_smtbmc.py
+++ b/sbysrc/sby_engine_smtbmc.py
@@ -60,6 +60,10 @@ def run(mode, job, engine_idx, engine):
         logfile_prefix += "_induction"
         smtbmc_opts.append("-i")
 
+    if mode == "cover":
+        smtbmc_opts.append("-c")
+        trace_prefix += "%"
+
     task = SbyTask(job, taskname, job.model(model_name),
             ("cd %s; yosys-smtbmc --noprogress %s -t %d --dump-vcd %s.vcd --dump-vlogtb %s_tb.v --dump-smtc %s.smtc model/design_smt2.smt2") %
                     (job.workdir, " ".join(smtbmc_opts), job.opt_depth, trace_prefix, trace_prefix, trace_prefix),
@@ -85,12 +89,12 @@ def run(mode, job, engine_idx, engine):
     def exit_callback(retcode):
         assert task_status is not None
 
-        if mode == "bmc":
+        if mode == "bmc" or mode == "cover":
             job.status = task_status
             job.log("engine_%d: Status returned by engine: %s" % (engine_idx, task_status))
             job.summary.append("engine_%d (%s) returned %s" % (engine_idx, " ".join(engine), job.status))
 
-            if job.status == "FAIL":
+            if job.status == "FAIL" and mode != "cover":
                 job.summary.append("counterexample trace: %s/engine_%d/trace.vcd" % (job.workdir, engine_idx))
 
             job.terminate()

diff --git a/sbysrc/sby_mode_cover.py b/sbysrc/sby_mode_cover.py
new file mode 100644 (file)
index 0000000..78a59f9
--- /dev/null
+++ b/sbysrc/sby_mode_cover.py
@@ -0,0 +1,43 @@
+#
+# SymbiYosys (sby) -- Front-end for Yosys-based formal verification flows
+#
+# Copyright (C) 2016  Clifford Wolf <clifford@clifford.at>
+#
+# Permission to use, copy, modify, and/or distribute this software for any
+# purpose with or without fee is hereby granted, provided that the above
+# copyright notice and this permission notice appear in all copies.
+#
+# THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
+# WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
+# MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
+# ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
+# WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
+# ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
+# OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
+#
+
+import re, os, getopt
+from sby_core import SbyTask
+
+def run(job):
+    job.opt_depth = 20
+
+    if "depth" in job.options:
+        job.opt_depth = int(job.options["depth"])
+
+    for engine_idx in range(len(job.engines)):
+        engine = job.engines[engine_idx]
+        assert len(engine) > 0
+
+        job.log("engine_%d: %s" % (engine_idx, " ".join(engine)))
+        os.makedirs("%s/engine_%d" % (job.workdir, engine_idx))
+
+        if engine[0] == "smtbmc":
+            import sby_engine_smtbmc
+            sby_engine_smtbmc.run("cover", job, engine_idx, engine)
+
+        else:
+            assert False
+
+    job.taskloop()
+