From: Clifford Wolf <clifford@clifford.at>
Date: Fri, 29 Jun 2018 16:21:38 +0000 (+0200)
Subject: Update remaining quickstart examples
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2fa29974dd32d069c790fe05cdb4de3ed767c47c;p=SymbiYosys.git

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 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.sv b/docs/examples/quickstart/cover.sv
new file mode 100644
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
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 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.sv b/docs/examples/quickstart/memory.sv
new file mode 100644
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
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 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.sv b/docs/examples/quickstart/prove.sv
new file mode 100644
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
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 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