From 2fa29974dd32d069c790fe05cdb4de3ed767c47c Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Fri, 29 Jun 2018 18:21:38 +0200
Subject: [PATCH] Update remaining quickstart examples

Signed-off-by: Clifford Wolf <clifford@clifford.at>
---
 docs/examples/quickstart/cover.sby               |  4 ++--
 docs/examples/quickstart/{cover.v => cover.sv}   |  8 ++++++--
 docs/examples/quickstart/memory.sby              |  4 ++--
 docs/examples/quickstart/{memory.v => memory.sv} |  2 +-
 docs/examples/quickstart/prove.sby               |  4 ++--
 docs/examples/quickstart/{prove.v => prove.sv}   | 10 +++++++---
 docs/source/quickstart.rst                       |  4 ++--
 7 files changed, 22 insertions(+), 14 deletions(-)
 rename docs/examples/quickstart/{cover.v => cover.sv} (56%)
 rename docs/examples/quickstart/{memory.v => memory.sv} (97%)
 rename docs/examples/quickstart/{prove.v => prove.sv} (81%)

diff --git a/docs/examples/quickstart/cover.sby b/docs/examples/quickstart/cover.sby
index 58cce3a..4f60625 100644
--- a/docs/examples/quickstart/cover.sby
+++ b/docs/examples/quickstart/cover.sby
@@ -5,8 +5,8 @@ mode cover
 smtbmc
 
 [script]
-read_verilog -formal cover.v
+read -formal cover.sv
 prep -top top
 
 [files]
-cover.v
+cover.sv
diff --git a/docs/examples/quickstart/cover.v b/docs/examples/quickstart/cover.sv
similarity index 56%
rename from docs/examples/quickstart/cover.v
rename to docs/examples/quickstart/cover.sv
index 4b0d475..478ce36 100644
--- a/docs/examples/quickstart/cover.v
+++ b/docs/examples/quickstart/cover.sv
@@ -8,6 +8,10 @@ module top (
 		state <= ((state << 5) + state) ^ din;
 	end
 
-	cover property (state == 'd 12345678);
-	cover property (state == 'h 12345678);
+`ifdef FORMAL
+	always @(posedge clk) begin
+		cover (state == 'd 12345678);
+		cover (state == 'h 12345678);
+	end
+`endif
 endmodule
diff --git a/docs/examples/quickstart/memory.sby b/docs/examples/quickstart/memory.sby
index 066c023..540c094 100644
--- a/docs/examples/quickstart/memory.sby
+++ b/docs/examples/quickstart/memory.sby
@@ -7,8 +7,8 @@ expect fail
 smtbmc boolector
 
 [script]
-read_verilog -formal memory.v
+read -formal memory.sv
 prep -top testbench
 
 [files]
-memory.v
+memory.sv
diff --git a/docs/examples/quickstart/memory.v b/docs/examples/quickstart/memory.sv
similarity index 97%
rename from docs/examples/quickstart/memory.v
rename to docs/examples/quickstart/memory.sv
index 49e7dff..fdb9ca4 100644
--- a/docs/examples/quickstart/memory.v
+++ b/docs/examples/quickstart/memory.sv
@@ -12,7 +12,7 @@ module testbench (
     .rdata(rdata)
   );
 
-  wire [9:0] test_addr = $anyconst;
+  (* anyconst *) reg [9:0] test_addr;
   reg test_data_valid = 0;
   reg [7:0] test_data;
 
diff --git a/docs/examples/quickstart/prove.sby b/docs/examples/quickstart/prove.sby
index 0f6f535..a83fcd5 100644
--- a/docs/examples/quickstart/prove.sby
+++ b/docs/examples/quickstart/prove.sby
@@ -5,8 +5,8 @@ mode prove
 smtbmc
 
 [script]
-read_verilog -formal prove.v
+read -formal prove.sv
 prep -top testbench
 
 [files]
-prove.v
+prove.sv
diff --git a/docs/examples/quickstart/prove.v b/docs/examples/quickstart/prove.sv
similarity index 81%
rename from docs/examples/quickstart/prove.v
rename to docs/examples/quickstart/prove.sv
index 4535368..72b353e 100644
--- a/docs/examples/quickstart/prove.v
+++ b/docs/examples/quickstart/prove.sv
@@ -8,11 +8,15 @@ module testbench (
     .clk  (clk  ),
     .reset(reset),
     .din  (din  ),
-    .dout (dout ),
+    .dout (dout )
   );
 
-  initial assume (reset);
-  assert property (reset || !dout[1:0]);
+  reg init = 1;
+  always @(posedge clk) begin
+    if (init) assume (reset);
+    if (!reset) assert (!dout[1:0]);
+    init <= 0;
+  end
 endmodule
 
 module demo (
diff --git a/docs/source/quickstart.rst b/docs/source/quickstart.rst
index 2a170e8..e5b7d5b 100644
--- a/docs/source/quickstart.rst
+++ b/docs/source/quickstart.rst
@@ -190,7 +190,7 @@ also be a useful method for evaluating engines.)
 
 Let's consider the following example:
 
-.. literalinclude:: ../examples/quickstart/memory.v
+.. literalinclude:: ../examples/quickstart/memory.sv
    :language: systemverilog
 
 This example is expected to fail verification (see the BUG comment).
@@ -224,7 +224,7 @@ Bounded model checks only prove that the safety properties hold for the first
 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
+.. literalinclude:: ../examples/quickstart/prove.sv
    :language: systemverilog
 
 Proving this design in an unbounded manner can be achieved using the following
-- 
2.30.2