Add some docs for "prove" mode

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

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

diff --git a/docs/examples/quickstart/prove.v b/docs/examples/quickstart/prove.v
new file mode 100644 (file)
index 0000000..d9a55da
--- /dev/null
+++ b/docs/examples/quickstart/prove.v
@@ -0,0 +1,49 @@
+module testbench (
+  input clk,
+  input reset,
+  input [7:0] din,
+  output reg [7:0] dout
+);
+  demo uut (
+    .clk  (clk  ),
+    .reset(reset),
+    .din  (din  ),
+    .dout (dout ),
+  );
+
+  initial assume (reset);
+  assert property (reset || !dout[1:0]);
+endmodule
+
+module demo (
+  input clk,
+  input reset,
+  input [7:0] din,
+  output reg [7:0] dout
+);
+  reg [7:0] buffer;
+  reg [2:0] state;
+
+  always @(posedge clk) begin
+    if (reset) begin
+      dout <= 0;
+      state <= 0;
+    end else
+    case (state)
+      3'b 001: begin
+        buffer <= din;
+       state <= 1;
+      end
+      3'b 010: begin
+        if (buffer[1:0])
+         buffer <= buffer + 1;
+       else
+         state <= 2;
+      end
+      3'b 100: begin
+        dout <= dout + buffer;
+       state <= 0;
+      end
+    endcase
+  end
+endmodule

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

diff --git a/docs/source/quickstart.rst b/docs/source/quickstart.rst
index 6bcc1073c81f61debd72c5a1d3bf08025d64ff37..cec67d7ebbefca4e41e2c17066bcfdfecd2a9223 100644 (file)
--- a/docs/source/quickstart.rst
+++ b/docs/source/quickstart.rst
@@ -116,6 +116,22 @@ can either engine verify the design when the bug has been fixed?
 Beyond bounded model checks
 ---------------------------
 
-TBD
+Bounded model checks only prove that the safety properties hold for the first
+*N* cycles (where *N* is the depth of the BMC). Sometimes this is insufficient
+and we need to prove that the safety properties hold forever, not just the first
+*N* cycles. Let us consider the following example:
+
+.. literalinclude:: ../examples/quickstart/prove.v
+   :language: systemverilog
+
+Proving this design in an unbounded manner can be achieved using the following
+SymbiYosys configuration file:
+
+.. literalinclude:: ../examples/quickstart/prove.sby
+   :language: text
 
+Note that ``mode`` is now set to ``prove`` instead of ``bmc``. The ``smtbmc``
+engine in ``prove`` mode will perform a k-induction proof. Other engines can
+use other methods, e.g. using ``abc pdr`` will prove the design using the IC3
+algorithm.
 

diff --git a/sbysrc/sby_engine_smtbmc.py b/sbysrc/sby_engine_smtbmc.py
index 65ebbc6c82eac86e629963f13fa49d7f00003964..f717beec4aa2bd041738578da988de1393a2d650 100644 (file)
--- a/sbysrc/sby_engine_smtbmc.py
+++ b/sbysrc/sby_engine_smtbmc.py
@@ -52,11 +52,12 @@ def run(mode, job, engine_idx, engine):
 
     if mode == "prove_basecase":
         taskname += ".basecase"
+        logfile_prefix += "_basecase"
 
     if mode == "prove_induction":
         taskname += ".induction"
         trace_prefix += "_induct"
-        logfile_prefix += "_induct"
+        logfile_prefix += "_induction"
         smtbmc_opts.append("-i")
 
     task = SbyTask(job, taskname, job.model(model_name),