Update remaining quickstart examples

Signed-off-by: Clifford Wolf <clifford@clifford.at>

diff --git a/docs/examples/quickstart/cover.sby b/docs/examples/quickstart/cover.sby
index 58cce3adfc066ec0a0cd0a0448bcd46356beb867..4f60625a54316d5110a0422a1e1588926a9e57e5 100644 (file)
--- 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.sv b/docs/examples/quickstart/cover.sv
new file mode 100644 (file)
index 0000000..478ce36
--- /dev/null
+++ b/docs/examples/quickstart/cover.sv
@@ -0,0 +1,17 @@
+module top (
+       input clk,
+       input [7:0] din
+);
+       reg [31:0] state = 0;
+
+       always @(posedge clk) begin
+               state <= ((state << 5) + state) ^ din;
+       end
+
+`ifdef FORMAL
+       always @(posedge clk) begin
+               cover (state == 'd 12345678);
+               cover (state == 'h 12345678);
+       end
+`endif
+endmodule

diff --git a/docs/examples/quickstart/cover.v b/docs/examples/quickstart/cover.v
deleted file mode 100644 (file)
index 4b0d475..0000000
--- a/docs/examples/quickstart/cover.v
+++ /dev/null
@@ -1,13 +0,0 @@
-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/examples/quickstart/memory.sby b/docs/examples/quickstart/memory.sby
index 066c0231a913869a3ff507904b7f4c645920be8e..540c094b84bc542cea9d8a4dbd8377e9169a17a6 100644 (file)
--- 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.sv b/docs/examples/quickstart/memory.sv
new file mode 100644 (file)
index 0000000..fdb9ca4
--- /dev/null
+++ b/docs/examples/quickstart/memory.sv
@@ -0,0 +1,60 @@
+module testbench (
+  input clk, wen,
+  input [9:0] addr,
+  input [7:0] wdata,
+  output [7:0] rdata
+);
+  memory uut (
+    .clk  (clk  ),
+    .wen  (wen  ),
+    .addr (addr ),
+    .wdata(wdata),
+    .rdata(rdata)
+  );
+
+  (* anyconst *) reg [9:0] test_addr;
+  reg test_data_valid = 0;
+  reg [7:0] test_data;
+
+  always @(posedge clk) begin
+    if (addr == test_addr) begin
+      if (wen) begin
+        test_data <= wdata;
+       test_data_valid <= 1;
+      end
+      if (test_data_valid) begin
+        assert(test_data == rdata);
+      end
+    end
+  end
+endmodule
+
+module memory (
+  input clk, wen,
+  input [9:0] addr,
+  input [7:0] wdata,
+  output [7:0] rdata
+);
+  reg [7:0] bank0 [0:255];
+  reg [7:0] bank1 [0:255];
+  reg [7:0] bank2 [0:255];
+  reg [7:0] bank3 [0:255];
+
+  wire [1:0] mem_sel = addr[9:8];
+  wire [7:0] mem_addr = addr[7:0];
+
+  always @(posedge clk) begin
+    case (mem_sel)
+      0: if (wen) bank0[mem_addr] <= wdata;
+      1: if (wen) bank1[mem_addr] <= wdata;
+      2: if (wen) bank1[mem_addr] <= wdata;  // BUG: Should assign to bank2
+      3: if (wen) bank3[mem_addr] <= wdata;
+    endcase
+  end
+
+  assign rdata =
+    mem_sel == 0 ? bank0[mem_addr] :
+    mem_sel == 1 ? bank1[mem_addr] :
+    mem_sel == 2 ? bank2[mem_addr] :
+    mem_sel == 3 ? bank3[mem_addr] : 'bx;
+endmodule

diff --git a/docs/examples/quickstart/memory.v b/docs/examples/quickstart/memory.v
deleted file mode 100644 (file)
index 49e7dff..0000000
--- a/docs/examples/quickstart/memory.v
+++ /dev/null
@@ -1,60 +0,0 @@
-module testbench (
-  input clk, wen,
-  input [9:0] addr,
-  input [7:0] wdata,
-  output [7:0] rdata
-);
-  memory uut (
-    .clk  (clk  ),
-    .wen  (wen  ),
-    .addr (addr ),
-    .wdata(wdata),
-    .rdata(rdata)
-  );
-
-  wire [9:0] test_addr = $anyconst;
-  reg test_data_valid = 0;
-  reg [7:0] test_data;
-
-  always @(posedge clk) begin
-    if (addr == test_addr) begin
-      if (wen) begin
-        test_data <= wdata;
-       test_data_valid <= 1;
-      end
-      if (test_data_valid) begin
-        assert(test_data == rdata);
-      end
-    end
-  end
-endmodule
-
-module memory (
-  input clk, wen,
-  input [9:0] addr,
-  input [7:0] wdata,
-  output [7:0] rdata
-);
-  reg [7:0] bank0 [0:255];
-  reg [7:0] bank1 [0:255];
-  reg [7:0] bank2 [0:255];
-  reg [7:0] bank3 [0:255];
-
-  wire [1:0] mem_sel = addr[9:8];
-  wire [7:0] mem_addr = addr[7:0];
-
-  always @(posedge clk) begin
-    case (mem_sel)
-      0: if (wen) bank0[mem_addr] <= wdata;
-      1: if (wen) bank1[mem_addr] <= wdata;
-      2: if (wen) bank1[mem_addr] <= wdata;  // BUG: Should assign to bank2
-      3: if (wen) bank3[mem_addr] <= wdata;
-    endcase
-  end
-
-  assign rdata =
-    mem_sel == 0 ? bank0[mem_addr] :
-    mem_sel == 1 ? bank1[mem_addr] :
-    mem_sel == 2 ? bank2[mem_addr] :
-    mem_sel == 3 ? bank3[mem_addr] : 'bx;
-endmodule

diff --git a/docs/examples/quickstart/prove.sby b/docs/examples/quickstart/prove.sby
index 0f6f535770a99769ce41f96c612def06c1d374c7..a83fcd554b64eab8bff6426b49e8a2b187d29f20 100644 (file)
--- 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.sv b/docs/examples/quickstart/prove.sv
new file mode 100644 (file)
index 0000000..72b353e
--- /dev/null
+++ b/docs/examples/quickstart/prove.sv
@@ -0,0 +1,53 @@
+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 )
+  );
+
+  reg init = 1;
+  always @(posedge clk) begin
+    if (init) assume (reset);
+    if (!reset) assert (!dout[1:0]);
+    init <= 0;
+  end
+endmodule
+
+module demo (
+  input clk,
+  input reset,
+  input [7:0] din,
+  output reg [7:0] dout
+);
+  reg [7:0] buffer;
+  reg [1:0] state;
+
+  always @(posedge clk) begin
+    if (reset) begin
+      dout <= 0;
+      state <= 0;
+    end else
+    case (state)
+      0: begin
+        buffer <= din;
+       state <= 1;
+      end
+      1: begin
+        if (buffer[1:0])
+         buffer <= buffer + 1;
+       else
+         state <= 2;
+      end
+      2: begin
+        dout <= dout + buffer;
+       state <= 0;
+      end
+    endcase
+  end
+endmodule

diff --git a/docs/examples/quickstart/prove.v b/docs/examples/quickstart/prove.v
deleted file mode 100644 (file)
index 4535368..0000000
--- a/docs/examples/quickstart/prove.v
+++ /dev/null
@@ -1,49 +0,0 @@
-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 [1:0] state;
-
-  always @(posedge clk) begin
-    if (reset) begin
-      dout <= 0;
-      state <= 0;
-    end else
-    case (state)
-      0: begin
-        buffer <= din;
-       state <= 1;
-      end
-      1: begin
-        if (buffer[1:0])
-         buffer <= buffer + 1;
-       else
-         state <= 2;
-      end
-      2: begin
-        dout <= dout + buffer;
-       state <= 0;
-      end
-    endcase
-  end
-endmodule

diff --git a/docs/source/quickstart.rst b/docs/source/quickstart.rst
index 2a170e8e21855c0a09371db7371de887aae53406..e5b7d5b720e6e16cd4f81bcb328e406e5786cd8d 100644 (file)
--- 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