From 770c6441d8f8045e8dc2a6686d3cbea60e98fea4 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Wed, 13 Dec 2017 19:17:20 +0100
Subject: [PATCH] Add dpmem multiclk example

---
 docs/examples/multiclk/.gitignore |  1 +
 docs/examples/multiclk/dpmem.sby  | 17 +++++++++
 docs/examples/multiclk/dpmem.sv   | 60 +++++++++++++++++++++++++++++++
 3 files changed, 78 insertions(+)
 create mode 100644 docs/examples/multiclk/.gitignore
 create mode 100644 docs/examples/multiclk/dpmem.sby
 create mode 100644 docs/examples/multiclk/dpmem.sv

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