Add dpmem multiclk example

diff --git a/docs/examples/multiclk/.gitignore b/docs/examples/multiclk/.gitignore
new file mode 100644 (file)
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 (file)
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 (file)
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