sbysrc/demo3.sby

   1 [options]
   2 depth 10
   3 mode bmc
   4
   5 [engines]
   6 smtbmc yices
   7
   8 [script]
   9 read_verilog -formal demo.v
  10 prep -top top
  11
  12 [file demo.v]
  13 module top (
  14   input clk,
  15   input [7:0] addr,
  16   input [7:0] wdata,
  17   output [7:0] rdata
  18 );
  19   rand const reg [7:0] test_addr;
  20   reg [7:0] test_data;
  21   reg test_valid = 0;
  22
  23   always @(posedge clk) begin
  24     if (addr == test_addr) begin
  25       if (test_valid)
  26         assert(test_data == rdata);
  27       test_data <= wdata;
  28       test_valid <= 1;
  29     end
  30   end
  31
  32   memory uut (
  33     .clk  (clk  ),
  34     .addr (addr ),
  35     .wdata(wdata),
  36     .rdata(rdata)
  37   );
  38 endmodule
  39
  40
  41 module memory (
  42   input clk,
  43   input [7:0] addr,
  44   input [7:0] wdata,
  45   output [7:0] rdata
  46 );
  47   reg [7:0] mem [0:255];
  48
  49   always @(posedge clk)
  50     mem[addr] <= wdata;
  51
  52   assign rdata = mem[addr];
  53 endmodule