From 14bfd3c5c159626a2b3b8dec3a446e0f7c4c7e0c Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Thu, 8 Sep 2016 11:16:12 +0200 Subject: yosys-smtbmc meminit support --- examples/smtbmc/demo7.v | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) create mode 100644 examples/smtbmc/demo7.v (limited to 'examples/smtbmc/demo7.v') 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 -- cgit v1.2.3