Update quickstart demo

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

diff --git a/docs/examples/quickstart/demo.sby b/docs/examples/quickstart/demo.sby
index 01fb2aaadb510f2fa5cfcd1e870cea0117a4db2a..0e8fdcf733b06b659fe328ad8239fc5bb84bdf9e 100644 (file)
--- a/docs/examples/quickstart/demo.sby
+++ b/docs/examples/quickstart/demo.sby
@@ -6,8 +6,8 @@ depth 100
 smtbmc
 
 [script]
-read_verilog -formal demo.v
+read -formal demo.sv
 prep -top demo
 
 [files]
-demo.v
+demo.sv

diff --git a/docs/examples/quickstart/demo.sv b/docs/examples/quickstart/demo.sv
new file mode 100644 (file)
index 0000000..0184df4
--- /dev/null
+++ b/docs/examples/quickstart/demo.sv
@@ -0,0 +1,19 @@
+module demo (
+  input clk,
+  output [5:0] counter
+);
+  reg [5:0] counter = 0;
+
+  always @(posedge clk) begin
+    if (counter == 50)
+      counter <= 0;
+    else
+      counter <= counter + 1;
+  end
+
+`ifdef FORMAL
+  always @(posedge clk) begin
+    assert (counter < 32);
+  end
+`endif
+endmodule

diff --git a/docs/examples/quickstart/demo.v b/docs/examples/quickstart/demo.v
deleted file mode 100644 (file)
index 09044de..0000000
--- a/docs/examples/quickstart/demo.v
+++ /dev/null
@@ -1,15 +0,0 @@
-module demo (
-  input clk,
-  output [5:0] counter
-);
-  reg [5:0] counter = 0;
-
-  always @(posedge clk) begin
-    if (counter == 15)
-      counter <= 0;
-    else
-      counter <= counter + 1;
-  end
-
-  assert property (counter < 32);
-endmodule

diff --git a/docs/source/quickstart.rst b/docs/source/quickstart.rst
index e722c1979ef13db009e1df685c372399a3cc88ee..2a170e8e21855c0a09371db7371de887aae53406 100644 (file)
--- a/docs/source/quickstart.rst
+++ b/docs/source/quickstart.rst
@@ -129,7 +129,7 @@ First step: A simple BMC example
 
 Here is a simple example design with a safety property (assertion).
 
-.. literalinclude:: ../examples/quickstart/demo.v
+.. literalinclude:: ../examples/quickstart/demo.sv
    :language: systemverilog
 
 The property in this example is true. We'd like to verify this using a bounded
@@ -141,7 +141,7 @@ configure SymbiYosys to run a BMC for 100 cycles on the design:
 .. literalinclude:: ../examples/quickstart/demo.sby
    :language: text
 
-Simply create a text file ``demo.v`` with the example design and another text
+Simply create a text file ``demo.sv`` with the example design and another text
 file ``demo.sby`` with the SymbiYosys configuration. Then run::
 
    sby demo.sby