From: Clifford Wolf <clifford@clifford.at>
Date: Mon, 5 Mar 2018 23:03:54 +0000 (+0100)
Subject: Add fib example using tasks
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=951211856da857aa56995c2eabf587c4b8cd6405;p=SymbiYosys.git

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
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
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