Add dpmem multiclk example

docs/examples/multiclk/.gitignore

@@ -0,0 +1 @@
+/dpmem/

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

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