diff options
Diffstat (limited to 'examples/smtbmc/demo7.v')
-rw-r--r-- | examples/smtbmc/demo7.v | 18 |
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 |