tests/prv32fmcmp.v

   1 module prv32fmcmp (
   2         input         clock,
   3         input         resetn,
   4         output        mem_valid_a, mem_valid_b,
   5         output        mem_instr_a, mem_instr_b,
   6         input         mem_ready_a, mem_ready_b,
   7         output [31:0] mem_addr_a, mem_addr_b,
   8         output [31:0] mem_wdata_a, mem_wdata_b,
   9         output [ 3:0] mem_wstrb_a, mem_wstrb_b,
  10         input  [31:0] mem_rdata_a, mem_rdata_b
  11 );
  12         picorv32 #(
  13                 .REGS_INIT_ZERO(1),
  14                 .COMPRESSED_ISA(1)
  15         ) prv32_a (
  16                 .clk       (clock      ),
  17                 .resetn    (resetn     ),
  18                 .mem_valid (mem_valid_a),
  19                 .mem_instr (mem_instr_a),
  20                 .mem_ready (mem_ready_a),
  21                 .mem_addr  (mem_addr_a ),
  22                 .mem_wdata (mem_wdata_a),
  23                 .mem_wstrb (mem_wstrb_a),
  24                 .mem_rdata (mem_rdata_a)
  25         );
  26
  27         picorv32 #(
  28                 .REGS_INIT_ZERO(1),
  29                 .COMPRESSED_ISA(1)
  30         ) prv32_b (
  31                 .clk       (clock      ),
  32                 .resetn    (resetn     ),
  33                 .mem_valid (mem_valid_b),
  34                 .mem_instr (mem_instr_b),
  35                 .mem_ready (mem_ready_b),
  36                 .mem_addr  (mem_addr_b ),
  37                 .mem_wdata (mem_wdata_b),
  38                 .mem_wstrb (mem_wstrb_b),
  39                 .mem_rdata (mem_rdata_b)
  40         );
  41
  42         reg [31:0] rom [0:255];
  43
  44         integer mem_access_cnt_a = 0;
  45         integer mem_access_cnt_b = 0;
  46
  47         always @* begin
  48                 assume(resetn == !$initstate);
  49
  50                 if (resetn) begin
  51                         // only consider programs without data memory read/write
  52                         if (mem_valid_a) assume(mem_instr_a);
  53                         if (mem_valid_b) assume(mem_instr_b);
  54
  55                         // when the access cnt matches, the addresses must match
  56                         if (mem_valid_a && mem_valid_b && mem_access_cnt_a == mem_access_cnt_b) begin
  57                                 assert(mem_addr_a == mem_addr_b);
  58                         end
  59
  60                         // hook up to memory
  61                         assume(mem_rdata_a == rom[mem_addr_a[9:2]]);
  62                         assume(mem_rdata_b == rom[mem_addr_b[9:2]]);
  63                 end
  64
  65                 // it will pass when this is enabled
  66                 //assume(mem_ready_a == mem_ready_b);
  67         end
  68
  69         always @(posedge clock) begin
  70                 mem_access_cnt_a <= mem_access_cnt_a + (resetn && mem_valid_a && mem_ready_a);
  71                 mem_access_cnt_b <= mem_access_cnt_b + (resetn && mem_valid_b && mem_ready_b);
  72         end
  73 endmodule