From: Clifford Wolf <clifford@clifford.at>
Date: Wed, 13 Dec 2017 18:17:20 +0000 (+0100)
Subject: Add dpmem multiclk example
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=770c6441d8f8045e8dc2a6686d3cbea60e98fea4;p=SymbiYosys.git

Add dpmem multiclk example
---

diff --git a/docs/examples/multiclk/.gitignore b/docs/examples/multiclk/.gitignore
new file mode 100644
index 0000000..3bd1ca8
--- /dev/null
+++ b/docs/examples/multiclk/.gitignore
@@ -0,0 +1 @@
+/dpmem/
diff --git a/docs/examples/multiclk/dpmem.sby b/docs/examples/multiclk/dpmem.sby
new file mode 100644
index 0000000..08e44a6
--- /dev/null
+++ b/docs/examples/multiclk/dpmem.sby
@@ -0,0 +1,17 @@
+[options]
+mode bmc
+depth 15
+
+[engines]
+smtbmc
+
+[script]
+read_verilog -sv -formal dpmem.sv
+prep -nordff -top top
+memory_map
+chformal -early -assume
+clk2fflogic
+opt_clean
+
+[files]
+dpmem.sv
diff --git a/docs/examples/multiclk/dpmem.sv b/docs/examples/multiclk/dpmem.sv
new file mode 100644
index 0000000..46d9872
--- /dev/null
+++ b/docs/examples/multiclk/dpmem.sv
@@ -0,0 +1,60 @@
+module dpmem (
+	input            rc,
+	input      [3:0] ra,
+	output reg [3:0] rd,
+
+	input            wc,
+	input            we,
+	input      [3:0] wa,
+	input      [3:0] wd
+);
+	reg [3:0] mem [0:15];
+
+	always @(posedge rc) begin
+		rd <= mem[ra];
+	end
+
+	always @(posedge wc) begin
+		if (we) mem[wa] <= wd;
+	end
+endmodule
+
+module top (
+	input            rc,
+	input      [3:0] ra,
+	output     [3:0] rd,
+
+	input            wc,
+	input            we,
+	input      [3:0] wa,
+	input      [3:0] wd
+);
+	dpmem uut (
+		.rc(rc),
+		.ra(ra),
+		.rd(rd),
+		.wc(wc),
+		.we(we),
+		.wa(wa),
+		.wd(wd)
+	);
+
+	reg shadow_valid = 0;
+	reg [3:0] shadow_data;
+	const rand reg [3:0] shadow_addr;
+
+	always @($global_clock) begin
+		assume($stable(rc) || $stable(wc));
+
+		if (!$initstate) begin
+			if ($rose(rc) && shadow_valid && shadow_addr == $past(ra)) begin
+				assert(shadow_data == rd);
+			end
+
+			if ($rose(wc) && $past(we) && shadow_addr == $past(wa)) begin
+				shadow_data <= $past(wd);
+				shadow_valid <= 1;
+			end
+		end
+	end
+endmodule