From: Clifford Wolf <clifford@clifford.at>
Date: Mon, 30 Jan 2017 12:23:07 +0000 (+0100)
Subject: Add some docs for "prove" mode
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1410ac4d49106036441db1b752085a97af3e3add;p=SymbiYosys.git

Add some docs for "prove" mode
---

diff --git a/docs/examples/quickstart/.gitignore b/docs/examples/quickstart/.gitignore
index 5a875a0..b0c09d4 100644
--- 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
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
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 9620eb3..daf29ba 100644
--- 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 6bcc107..cec67d7 100644
--- 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 65ebbc6..f717bee 100644
--- 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),