VERIFICATION ASYNCHRONOUS FIFO CUMMINGS

user49 · January 26, 2023, 6:42pm

In reply to GiuseppeT:

In reply to ben@SystemVerilog.us:
Mmh first of all, thank you so much for your patience with me. Really appreciating the fact that you’re doing everything that you can to lead me in the right direction.
By taking a look at your code example, I get why you’re suggesting me to use only one agent, because maybe in the Generator file I can randomize situation variable which is a typedef enum type and according to its value, I can do something in the case statement; like, if situation is == RD, then I am going to provide to the Driver Read_enable ==1, Write_enable==0 etc and basically I can do this for each case (correct me if I am wrong).

[Ben] You’re correct. In fact, the whole verification can be done in one module with no classes, but tasks would be helpful. But you have an assignment.

My problem with one Agent would be: how can I deal with the two asynchronous clocks in the interface, driver and monitor? Driver and Monitor work for sure with a clock signal, so how am I supposed to know which one to use? In my case, the Write_clock is faster than the read_clock, I cannot use the write_clock signal to drive the read signals to the interface from the Driver…does it make sense for you what I am trying to say? Hope it does

I understand your concern, but they are overdriven (exaggerated).
I am including a model from my SVA 4th edition assertion book. This model checks thru assertions a FIFO-like model where data is written at one rate(33MHz) into a black box is read at a slower rate(25MHz).

I emulated my FIFO black box with a queue
int dataQ [$]; // queue, to store/read incoming data
On Writes, I push front, syncked to the wr33 clk
if (wr_33) dataQ.push_front(wdata); // store data
On Reads, I pop from the back
rdata_from_q <= dataQ.pop_back();
To check that the data read is correct, I wrote this assertion


// Data integrity check
property p_read_data_integrity;
@(posedge clk_rcv25)
rd_25 |=>  rdata_from_q==rdata;
endproperty : p_read_data_integrity
ap_read_data_integrity : assert property (p_read_data_integrity);
// Assertion is equivalent to
// Updated 1/27/2023  See my paper rb.gy/mu4ttk
//
always @(posedge clk_rcv25)
if(rd_25) fork
do_check();
join_none
task automatic do_check();
@(posedge clk_rcv25) assert(rdata_from_q==rdata);
// same as **if (!(rdata_from_q==rdata)) $error;**
// I used the automatic task to avoid missing errors for continuous reads

As you can see, the monitor is the queue that can handle the writes and reads separately or concurrently. Study my model, and if you are serious about going into the design and verification field, take a close looks at my books (some free). I put a lot of efforts into them, and provided lots of real examples.

//   The data received from an interface (with wr control) must be properly 
//   transferred to the receiving hardware (with rd control).
//   The data is sourced at a 33 MHz rate and is extracted at a 25 MHz rate.
//   The receiver uses a ready4data signal to throttle the transmission
//   of one Kilo-words of data block.  The data extracted by the receiver
//   is in the same order that it was transmitted. 
module bus_xfr_data_integrity_check (
  input wr_33, // Transmitter write signal @33MHz
  input rd_25,  // Receiver   read signal @25 MHz
  input int wdata, // write data frofm Transmitter
  input int rdata, // read data from Receiver
  input reset_n, // active low reset
  input clk_xt33,   // clock transmitter @33 MHz
  input clk_rcv25); // clock Receiver @25 MHz
  timeunit 1ns;   timeprecision 100ps;

  parameter MAX_BUFF_SIZE=1024; 
//  int waddr;  // write address for storage of incoming data
//  int raddr;  // read address for reading of received data
  int rdata_from_q; // read data from queue to compare to Receiver
  int dataQ [$]; // queue, to store/read incoming data
  logic read_q_on_MT; // for waveform 
  
  logic[7:0] dataQ_size;
  assign dataQ_size  = dataQ.size; // dynamic arrays illegal in properties
  

  // Storage of data into queue
  always @ (posedge clk_xt33)
    if (reset_n==1'b0)
      dataQ 		 = {}; // clear the queue contents
    else begin
      if (wr_33) dataQ.push_front(wdata);  // store data
      end
  

  // Collect data from the Q 
  always @ (posedge clk_rcv25)
    if (rd_25 && dataQ_size!=0)  begin 
       rdata_from_q <= dataQ.pop_back();
	  read_q_on_MT 	<= 1'b0;
	  end 
     else begin 
       rdata_from_q <= 0;
	   read_q_on_MT <= 1'b1;
	 end     

  // Data integrity check 
  property p_read_data_integrity; 
    @(posedge clk_rcv25)
      rd_25 |=>  rdata_from_q==rdata;
  endproperty : p_read_data_integrity
  ap_read_data_integrity : assert property (p_read_data_integrity);

  // Never a READ with no data received
  property p_never_read_on_empty;
    @(posedge clk_rcv25)
      not (dataQ_size == 0 && rd_25);
  endproperty : p_never_read_on_empty
  ap_never_read_on_empty : assert property (p_never_read_on_empty);

  // never a write on a full buffer 
  property p_write_on_max_buff;
    @(posedge clk_xt33)
      not (dataQ_size == MAX_BUFF_SIZE && wr_33);
  endproperty : p_write_on_max_buff
  ap_write_on_max_buff : assert property (p_write_on_max_buff);


endmodule : bus_xfr_data_integrity_check
  
module top;
  timeunit 1ns;   timeprecision 100ps;
  logic wr_33=0; // Transmitter write signal @33MHz
  logic rd_25=0;  // Receiver   read signal @25 MHz
  int wdata; // write data from Transmitter
  int rdata; // read data from Receiver
  logic reset_n=1; // active low reset
  logic clk_xt33=1;   // clock transmitter @33 MHz
  logic clk_rcv25=1; // clock Receiver @25 MHz

  bus_xfr_data_integrity_check b_chk(.*);
  
  initial begin 
    reset_n =0;
	#100 reset_n =1;
  end  
  initial forever #30 clk_xt33=!clk_xt33;
  initial forever #40 clk_rcv25 =!clk_rcv25;
  always @ (posedge clk_xt33)
    assert(randomize(wr_33, wdata));
  always @ (posedge clk_rcv25)
    assert(randomize(rd_25, rdata));
endmodule : top