From: Clifford Wolf <clifford@clifford.at>
Date: Fri, 29 Jun 2018 08:05:52 +0000 (+0200)
Subject: Update quickstart demo
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=45a11da8eaf7685ff242590227960ef910adb906;p=SymbiYosys.git

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 01fb2aa..0e8fdcf 100644
--- 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
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
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 e722c19..2a170e8 100644
--- 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