extern/axicheck.v

   1 module testbench (
   2         input         clk,
   3         output        trap,
   4
   5         output        mem_axi_awvalid,
   6         input         mem_axi_awready,
   7         output [31:0] mem_axi_awaddr,
   8         output [ 2:0] mem_axi_awprot,
   9
  10         output        mem_axi_wvalid,
  11         input         mem_axi_wready,
  12         output [31:0] mem_axi_wdata,
  13         output [ 3:0] mem_axi_wstrb,
  14
  15         input         mem_axi_bvalid,
  16         output        mem_axi_bready,
  17
  18         output        mem_axi_arvalid,
  19         input         mem_axi_arready,
  20         output [31:0] mem_axi_araddr,
  21         output [ 2:0] mem_axi_arprot,
  22
  23         input         mem_axi_rvalid,
  24         output        mem_axi_rready,
  25         input  [31:0] mem_axi_rdata
  26 );
  27         reg resetn = 0;
  28
  29         always @(posedge clk)
  30                 resetn <= 1;
  31
  32         picorv32_axi #(
  33                 .ENABLE_COUNTERS(1),
  34                 .ENABLE_COUNTERS64(1),
  35                 .ENABLE_REGS_16_31(1),
  36                 .ENABLE_REGS_DUALPORT(1),
  37                 .BARREL_SHIFTER(1),
  38                 .TWO_CYCLE_COMPARE(0),
  39                 .TWO_CYCLE_ALU(0),
  40                 .COMPRESSED_ISA(0),
  41                 .CATCH_MISALIGN(1),
  42                 .CATCH_ILLINSN(1)
  43         ) uut (
  44                 .clk             (clk            ),
  45                 .resetn          (resetn         ),
  46                 .trap            (trap           ),
  47                 .mem_axi_awvalid (mem_axi_awvalid),
  48                 .mem_axi_awready (mem_axi_awready),
  49                 .mem_axi_awaddr  (mem_axi_awaddr ),
  50                 .mem_axi_awprot  (mem_axi_awprot ),
  51                 .mem_axi_wvalid  (mem_axi_wvalid ),
  52                 .mem_axi_wready  (mem_axi_wready ),
  53                 .mem_axi_wdata   (mem_axi_wdata  ),
  54                 .mem_axi_wstrb   (mem_axi_wstrb  ),
  55                 .mem_axi_bvalid  (mem_axi_bvalid ),
  56                 .mem_axi_bready  (mem_axi_bready ),
  57                 .mem_axi_arvalid (mem_axi_arvalid),
  58                 .mem_axi_arready (mem_axi_arready),
  59                 .mem_axi_araddr  (mem_axi_araddr ),
  60                 .mem_axi_arprot  (mem_axi_arprot ),
  61                 .mem_axi_rvalid  (mem_axi_rvalid ),
  62                 .mem_axi_rready  (mem_axi_rready ),
  63                 .mem_axi_rdata   (mem_axi_rdata  )
  64         );
  65
  66         reg expect_bvalid_aw = 0;
  67         reg expect_bvalid_w  = 0;
  68         reg expect_rvalid    = 0;
  69
  70         reg [3:0] timeout_aw = 0;
  71         reg [3:0] timeout_w  = 0;
  72         reg [3:0] timeout_b  = 0;
  73         reg [3:0] timeout_ar = 0;
  74         reg [3:0] timeout_r  = 0;
  75         reg [3:0] timeout_ex = 0;
  76
  77         always @(posedge clk) begin
  78                 timeout_aw <= !mem_axi_awvalid || mem_axi_awready ? 0 : timeout_aw + 1;
  79                 timeout_w  <= !mem_axi_wvalid  || mem_axi_wready  ? 0 : timeout_w  + 1;
  80                 timeout_b  <= !mem_axi_bvalid  || mem_axi_bready  ? 0 : timeout_b  + 1;
  81                 timeout_ar <= !mem_axi_arvalid || mem_axi_arready ? 0 : timeout_ar + 1;
  82                 timeout_r  <= !mem_axi_rvalid  || mem_axi_rready  ? 0 : timeout_r  + 1;
  83                 timeout_ex <= !{expect_bvalid_aw, expect_bvalid_w, expect_rvalid} ? 0 : timeout_ex + 1;
  84                 restrict(timeout_aw != 15);
  85                 restrict(timeout_w  != 15);
  86                 restrict(timeout_b  != 15);
  87                 restrict(timeout_ar != 15);
  88                 restrict(timeout_r  != 15);
  89                 restrict(timeout_ex != 15);
  90                 restrict(!trap);
  91
  92         end
  93
  94         always @(posedge clk) begin
  95                 if (resetn) begin
  96                         if (!$past(resetn)) begin
  97                                 assert(!mem_axi_awvalid);
  98                                 assert(!mem_axi_wvalid );
  99                                 assume(!mem_axi_bvalid );
 100                                 assert(!mem_axi_arvalid);
 101                                 assume(!mem_axi_rvalid );
 102                         end else begin
 103                                 // Only one read/write transaction in flight at each point in time
 104
 105                                 if (expect_bvalid_aw) begin
 106                                         assert(!mem_axi_awvalid);
 107                                 end
 108
 109                                 if (expect_bvalid_w) begin
 110                                         assert(!mem_axi_wvalid);
 111                                 end
 112
 113                                 if (expect_rvalid) begin
 114                                         assert(!mem_axi_arvalid);
 115                                 end
 116
 117                                 expect_bvalid_aw = expect_bvalid_aw || (mem_axi_awvalid && mem_axi_awready);
 118                                 expect_bvalid_w  = expect_bvalid_w  || (mem_axi_wvalid  && mem_axi_wready );
 119                                 expect_rvalid    = expect_rvalid    || (mem_axi_arvalid && mem_axi_arready);
 120
 121                                 if (expect_bvalid_aw || expect_bvalid_w) begin
 122                                         assert(!expect_rvalid);
 123                                 end
 124
 125                                 if (expect_rvalid) begin
 126                                         assert(!expect_bvalid_aw);
 127                                         assert(!expect_bvalid_w);
 128                                 end
 129
 130                                 if (!expect_bvalid_aw || !expect_bvalid_w) begin
 131                                         assume(!mem_axi_bvalid);
 132                                 end
 133
 134                                 if (!expect_rvalid) begin
 135                                         assume(!mem_axi_rvalid);
 136                                 end
 137
 138                                 if (mem_axi_bvalid && mem_axi_bready) begin
 139                                         expect_bvalid_aw = 0;
 140                                         expect_bvalid_w = 0;
 141                                 end
 142
 143                                 if (mem_axi_rvalid && mem_axi_rready) begin
 144                                         expect_rvalid = 0;
 145                                 end
 146
 147                                 // Check AXI Master Streams
 148
 149                                 if ($past(mem_axi_awvalid && !mem_axi_awready)) begin
 150                                         assert(mem_axi_awvalid);
 151                                         assert($stable(mem_axi_awaddr));
 152                                         assert($stable(mem_axi_awprot));
 153                                 end
 154                                 if ($fell(mem_axi_awvalid)) begin
 155                                         assert($past(mem_axi_awready));
 156                                 end
 157                                 if ($fell(mem_axi_awready)) begin
 158                                         assume($past(mem_axi_awvalid));
 159                                 end
 160
 161                                 if ($past(mem_axi_arvalid && !mem_axi_arready)) begin
 162                                         assert(mem_axi_arvalid);
 163                                         assert($stable(mem_axi_araddr));
 164                                         assert($stable(mem_axi_arprot));
 165                                 end
 166                                 if ($fell(mem_axi_arvalid)) begin
 167                                         assert($past(mem_axi_arready));
 168                                 end
 169                                 if ($fell(mem_axi_arready)) begin
 170                                         assume($past(mem_axi_arvalid));
 171                                 end
 172
 173                                 if ($past(mem_axi_wvalid && !mem_axi_wready)) begin
 174                                         assert(mem_axi_wvalid);
 175                                         assert($stable(mem_axi_wdata));
 176                                         assert($stable(mem_axi_wstrb));
 177                                 end
 178                                 if ($fell(mem_axi_wvalid)) begin
 179                                         assert($past(mem_axi_wready));
 180                                 end
 181                                 if ($fell(mem_axi_wready)) begin
 182                                         assume($past(mem_axi_wvalid));
 183                                 end
 184
 185                                 // Check AXI Slave Streams
 186
 187                                 if ($past(mem_axi_bvalid && !mem_axi_bready)) begin
 188                                         assume(mem_axi_bvalid);
 189                                 end
 190                                 if ($fell(mem_axi_bvalid)) begin
 191                                         assume($past(mem_axi_bready));
 192                                 end
 193                                 if ($fell(mem_axi_bready)) begin
 194                                         assert($past(mem_axi_bvalid));
 195                                 end
 196
 197                                 if ($past(mem_axi_rvalid && !mem_axi_rready)) begin
 198                                         assume(mem_axi_rvalid);
 199                                         assume($stable(mem_axi_rdata));
 200                                 end
 201                                 if ($fell(mem_axi_rvalid)) begin
 202                                         assume($past(mem_axi_rready));
 203                                 end
 204                                 if ($fell(mem_axi_rready)) begin
 205                                         assert($past(mem_axi_rvalid));
 206                                 end
 207                         end
 208                 end
 209         end
 210 endmodule