summaryrefslogtreecommitdiff
path: root/examples/smtbmc/demo7.v
diff options
context:
space:
mode:
Diffstat (limited to 'examples/smtbmc/demo7.v')
-rw-r--r--examples/smtbmc/demo7.v18
1 files changed, 18 insertions, 0 deletions
diff --git a/examples/smtbmc/demo7.v b/examples/smtbmc/demo7.v
new file mode 100644
index 00000000..75b3865c
--- /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