Checking order in fifo component

Hey guys.
Im new to formal verfication and sva my question is
How can i check that the data output go out in the same order it get in ?
What the auxiliary i should write ?

Thank you .

In reply to Michel_mor:
This queston is similar o the ones I address in my SVA book and at this forum.

https://verificationacademy.com/forums/systemverilog/need-help-write-assertion
https://verificationacademy.com/forums/systemverilog/assertion-expected-data-check/review-users-question

For this case, you need 2 flags: a tag and a serving variable.
Upon a wr, you save into the local variables of the property the tag, and the dada written into the fifo. You also increment the tag variable (to be used at the next w.


 int wr_tag, vdata; 
        (wr==1'b1, wr_tag=tag, inc_tag(), vdata=data) |=>  

Within that same property, you wait for the first occurence of a rd and the serving flag== to the locally stored flag. If that occurs, you then check that the read data is what ws saved as a write. The serving flag is incremented.


first_match(##[1:$] (rd && serving==wr_tag, inc_serving())) 
        ##0 read_data==vdata;  

// My testbench 
import uvm_pkg::*; `include "uvm_macros.svh" 
module top; 
    timeunit 1ns;     timeprecision 100ps;    
    bit clk,rd, wr;  
    int tag=0, serving=0, data=0, read_data=0; 
    default clocking @(posedge clk); 
    endclocking
    initial forever #10 clk=!clk; 
    // How can i check that the data output goes out in the same order it get in ?
    
    
    function void inc_tag();
        tag=tag+1'b1;
    endfunction
    
    function void inc_serving();
        serving=serving +1'b1; 
    endfunction
    
    property p_rdwr; 
        int wr_tag, vdata; 
        (wr==1'b1, wr_tag=tag, inc_tag(), vdata=data) |=> 
        first_match(##[1:$] (rd && serving==wr_tag, inc_serving())) 
        ##0 read_data==vdata; 
    endproperty 
    ap_reqack: assert property(p_rdwr);  
    // tag <=1'b0; else tag<= 1'b0; works for one 2nd req
    
    initial begin : init
        repeat(5)  begin : w0 // setup some writes 
            @(posedge clk); #1
            wr <= 1'b1; 
            rd <= 1'b0;
            data <= data+1'b1; 
        end : w0
        repeat(3)  begin : r0 // setup some reads 
            @(posedge clk); #1
            wr <= 1'b0; 
            rd <= 1'b1; 
           read_data <= read_data+ 1'b1; 
        end : r0
        repeat(200) begin : rpt // random 
            @(posedge clk); #1
            if (!randomize(rd, wr, read_data, data)  with 
            {rd dist {1'b1:=1, 1'b0:=3};
             wr dist {1'b1:=1, 1'b0:=1}; 
             data dist {7:=2, 9:=1};
             read_data dist {7:=2, 9:=1};}              
            ) `uvm_error("MYERR", "This is a randomize error");
        end : rpt
        $stop; 
    end : init
endmodule   

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr


  1. VF Horizons:PAPER: SVA Alternative for Complex Assertions | Verification Academy
  2. http://systemverilog.us/vf/SolvingComplexUsersAssertions.pdf
  3. “Using SVA for scoreboarding and TB designs”
    http://systemverilog.us/papers/sva4scoreboarding.pdf
  4. “Assertions Instead of FSMs/logic for Scoreboarding and Verification”
    October 2013 | Volume 9, Issue 3 | Verification Academy
  5. SVA in a UVM Class-based Environment
    SVA in a UVM Class-based Environment | Verification Horizons | Verification Academy

FREE BOOK: Component Design by Example
… A Step-by-Step Process Using VHDL with UART as Vehicle

thank you very much :)