Add fib example using tasks

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

diff --git a/docs/examples/demos/fib.sby b/docs/examples/demos/fib.sby
new file mode 100644 (file)
index 0000000..4622009
--- /dev/null
+++ b/docs/examples/demos/fib.sby
@@ -0,0 +1,28 @@
+[tasks]
+cover
+prove
+live
+
+[options]
+cover: mode cover
+prove: mode prove
+live:  mode live
+
+[engines]
+
+cover:
+smtbmc z3
+
+prove:
+abc pdr
+
+live:
+aiger suprove
+--
+
+[script]
+read_verilog -formal fib.v
+prep -top fib
+
+[files]
+fib.v

diff --git a/docs/examples/demos/fib.v b/docs/examples/demos/fib.v
new file mode 100644 (file)
index 0000000..016e75f
--- /dev/null
+++ b/docs/examples/demos/fib.v
@@ -0,0 +1,63 @@
+module fib (
+       input clk, pause, start,
+       input [3:0] n,
+       output reg busy, done,
+       output reg [9:0] f
+);
+       reg [3:0] count;
+       reg [9:0] q;
+
+       initial begin
+               done = 0;
+               busy = 0;
+       end
+
+       always @(posedge clk) begin
+               done <= 0;
+               if (!pause) begin
+                       if (!busy) begin
+                               if (start)
+                                       busy <= 1;
+                               count <= 0;
+                               q <= 1;
+                               f <= 0;
+                       end else begin
+                               q <= f;
+                               f <= f + q;
+                               count <= count + 1;
+                               if (count == n) begin
+                                       busy <= 0;
+                                       done <= 1;
+                               end
+                       end
+               end
+       end
+
+`ifdef FORMAL
+       always @(posedge clk) begin
+               if (busy) begin
+                       assume (!start);
+                       assume ($stable(n));
+               end
+
+               if (done) begin
+                       case ($past(n))
+                               0: assert (f == 1);
+                               1: assert (f == 1);
+                               2: assert (f == 2);
+                               3: assert (f == 3);
+                               4: assert (f == 5);
+                               5: assert (f == 8);
+                       endcase
+                       cover (f == 13);
+                       cover (f == 144);
+                       cover ($past(n) == 15);
+               end
+
+               assume (s_eventually !pause);
+
+               if (start && !pause)
+                       assert (s_eventually done);
+       end
+`endif
+endmodule