Hello,
I want to check ,for every request pulse there should be exactly two grant pulse otherwise it should throw failure.
I can use $past for this when it is known that grant will come after some fixed number of cycles ,but the requirement is that ,the two grant pulses can come at any number of cycles after request has come.
Is there any way to do it ?
In reply to pk_94:
// req forllowed by 2 grants
ap_req_grant_grant: assert property(@ (posedge clk)
$rose(req) |=> grant[->2] );
// No req until after the 2nd grant
// a grant cannot occur in the same cycle as req
ap_grant_noreq_grant: assert property(@ (posedge clk)
$rose(grant) |-> !req[*1:$] ##1 grant );
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr
In reply to VE:
That depends upon your requirements.
The assertions express that requirement.
Whar does your spec say?
Interesting that the assertion brought up the point of a possible weak set of requirements.
Ben systemverilog.us
In reply to ben@SystemVerilog.us:
Hi Ben,
Suppose there is another spec that says the following : -
1)There should be single gnt pulse for every req pulse made.
2)gnt can come between 1 to 100 clock cycle.
3)Its also possible that there can be another req pulse before the gnt of previous req pulse was completed (For example at time 0 there was req pulse and at time 3(say) there is another req pulse (till now there is no gnt for previous req pulses) so now if gnt comes it ,the following assertion would pass : -
req |-> ##[1:100] gnt.
One corner case scenario would be : - 10 req pulse came with single gnt (on say 11th cycle) but rest of the 9 gnts didn’t came.
Awaiting your reponse ben.
Thanks
In reply to pk_94:
You are correct that if you have 10 req pulse came with single gnt (on say 11th cycle) then you have 10 separate attempts all waiting for that ONE gnt. When the gnt arrives, it satisfies each of those 10 attempts.
(From my book) What is desired for this assertion is the exclusivity or uniqueness of each attempted thread sequences, meaning that one successful consequent does not terminate all concurrent attempts waiting for that consequent.
To accomplish this, one could use concepts of a familiar model seen in hardware stores in the paint department. There, the store provides a spool of tickets, each with a number. As a customer comes in, he takes a ticket. The clerk serving the customers has a sign that reads “NOW SERVING, TICKET x”. The customer that has the ticket gets served, the others have to wait. When done, the number X in incremented, and the next in-line customer gets served.
The assertion code could then be written as follows:
import uvm_pkg::*; `include "uvm_macros.svh"
module top;
timeunit 1ns; timeprecision 100ps;
bit clk,req, ack;
int ticket, now_serving;
default clocking @(posedge clk);
endclocking
initial forever #10 clk=!clk;
function void inc_ticket();
ticket = ticket + 1'b1;
endfunction
property reqack_unique;
int v_serving_ticket;
@(posedge clk) ($rose(req), v_serving_ticket=ticket, inc_ticket()) |->
##[1:10] now_serving==v_serving_ticket ##0 ack;
endproperty
ap_reqack_unique: assert property(reqack_unique)
now_serving =now_serving+1; else now_serving =now_serving+1;
initial begin
repeat(100) begin
@(posedge clk); #1;
if (!randomize(req, ack) with
{ req dist {1'b1:=1, 1'b0:=3};
ack dist {1'b1:=1, 1'b0:=5};
}) `uvm_error("MYERR", "This is a randomize error")
end
repeat(200) begin
@(posedge clk); #1
if (!randomize(req, ack) with
{ req dist {1'b1:=1, 1'b0:=3};
ack dist {1'b1:=0, 1'b0:=1};
}) `uvm_error("MYERR", "This is a randomize error")
end
$stop;
end
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
…
In reply to ben@SystemVerilog.us:
Thanks Ben for the explanation.I think you there is a typo in the following : -
ap_reqack_unique: assert property(reqack_unique)
now_serving =now_serving+1; else now_serving =now_serving+1;
Both the matching and non matching expression is same —> now_serving =now_serving+1
Same thing he, a PASS or a FAIL you want to increment the “now_serving” number to allow the next consequent of the req to be processed.
##[1:10] now_serving==v_serving_ticket ##0 ack;
Ben SystemVerilog.us
In reply to ben@SystemVerilog.us:
How about having the check in the monitor instead of assertions ?
class monitor;
virtual intf if1;
real reqque[$],gntque[$];
function new (virtual intf if1);
this.if1=if1;
endfunction
task load();
forever begin
@(posedge clk);
if(if1.req)
reqque.push_back($time);
if(if1.gnt) begin
gntque.push_back($time);
check();
end
end
endtask
task check();
real t1,t2;
t2=gntque.pop_front();
t1=reqque.pop_front();
if( t2-t1 > 5 )
`uvm_error("gnt violated the timing");
endtask
task run();
load();
endtask
endclass
In reply to verif_gal:
That would work though there are 2 issues to address:
Ben
@ben2 in your code
assertion ap_grant_noreq_grant will trigger for the second grant too right?
Expectation is to check that there is no req only after the first grant. After the second grant you will be seeing the req.
Please let me know if I am missing anything here.
Thanks.
// req forllowed by 2 grants
ap_req_grant_grant: assert property(@ (posedge clk)
$rose(req) |=> grant[->2] );
// No req until after the 2nd grant
// a grant cannot occur in the same cycle as req
ap_grant_noreq_grant: assert property(@ (posedge clk)
$rose(grant) |-> !req[*1:$] ##1 grant );
// [YOU] assertion ap_grant_noreq_grant will trigger for the second grant too right?
// Expectation is to check that there is no req only after the first grant.
//[Ben] $rose(grant) |-> !req[*1:$] ##1 grant );
// says that nfor every new grant, there is no req until another grant
// [YOU] After the second grant you will be seeing the req.
// [Ben] NO unless the 2nd grant is not a rose of grant.
// grants 0 0 0 0 1 1 1 0 0 1 0 0 1
// req 0 0 0 0 0 0 0 1 0 0 0 0 0
// ap_grant_noreq_grant ^ P // Thread1 pass
// ap_grant_noreq_grant * // no check on this req
// ap_grant_noreq_grant ^ P // Thread2 pass
// [Ben] You'll need to add support logic if you need exclusivity
Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.
Hi @ben2 ,
How about if the spec has a number_of_grants field sent with a request which states how many grants are required for that specific request? The number of grants are to be received within 100 cycles of the request, but a grant can be sent 2 cycles before its request. Similar to the previous one, the request can overlap, so a 2 requests might come in before the grants of the first is received, so the grants for both will have to be returned.
Thanks
/* SVA: 1)Number_of_grants per request is dynamically
2) All grants to be received within 100 cycles of the request
3) A grant can be sent 2 cycles before its request. */
int number_of_grants;
// assumptions here as to how the number of expected grants is obtained.
always number_of_grants=req_message[7:0]; // using support logic here
property ap_req_grant_grant; //untested
int v_numb, v_count; // number of grants, count of grants received
@ (posedge clk)
($rose(req), v_numb=number_of_grants, v_count=0) |->
(1, v_count+=$past(grant, 2)) // but a grant can be sent 2 cycles before its request.
(##1 (grant[->1], v_count+=1) [*1:$] intersect 1[*100]) // within 100 cycles of the request,
##0 v_numb==v_count;
endproperty
Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.