Update quickstart demo

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

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

docs/examples/quickstart/demo.sv

@@ -5,11 +5,15 @@ module demo (
   reg [5:0] counter = 0;
 
   always @(posedge clk) begin
-    if (counter == 15)
+    if (counter == 50)
       counter <= 0;
     else
       counter <= counter + 1;
   end
 
-  assert property (counter < 32);
+`ifdef FORMAL
+  always @(posedge clk) begin
+    assert (counter < 32);
+  end
+`endif
 endmodule

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