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
- SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
- A Pragmatic Approach to VMM Adoption 2006 ISBN 0-9705394-9-5
- Using PSL/SUGAR for Formal and Dynamic Verification 2nd Edition, 2004, ISBN 0-9705394-6-0
- Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 978-1539769712
- Component Design by Example ", 2001 ISBN 0-9705394-0-1
- VHDL Coding Styles and Methodologies, 2nd Edition, 1999 ISBN 0-7923-8474-1
- VHDL Answers to Frequently Asked Questions, 2nd Edition ISBN 0-7923-8115
- VF Horizons:PAPER: SVA Alternative for Complex Assertions | Verification Academy
- http://systemverilog.us/vf/SolvingComplexUsersAssertions.pdf
- “Using SVA for scoreboarding and TB designs”
http://systemverilog.us/papers/sva4scoreboarding.pdf - “Assertions Instead of FSMs/logic for Scoreboarding and Verification”
October 2013 | Volume 9, Issue 3 | Verification Academy - 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 :)