Add some docs for "prove" mode

docs/examples/quickstart/.gitignore

@@ -1,2 +1,3 @@
 demo
 memory
+prove

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

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

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]

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.
 

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),