yosys-smtbmc meminit support

1 files changed, 18 insertions, 0 deletions

diff --git a/examples/smtbmc/demo7.v b/examples/smtbmc/demo7.v
new file mode 100644
index 000000000..75b3865c5
--- /dev/null
+++ b/examples/smtbmc/demo7.v
@@ -0,0 +1,18 @@
+// Demo for memory initialization
+
+module demo7 (input [2:0] addr);
+	reg [15:0] memory [0:7];
+
+	initial begin
+		memory[0] = 1331;
+		memory[1] = 1331 + 1;
+		memory[2] = 1331 + 2;
+		memory[3] = 1331 + 4;
+		memory[4] = 1331 + 8;
+		memory[5] = 1331 + 16;
+		memory[6] = 1331 + 32;
+		memory[7] = 1331 + 64;
+	end
+
+	assert property (1000 < memory[addr] && memory[addr] < 2000);
+endmodule