hello everyone,
i am corrently working on axi master slave i have a problem on assertion writing and i want to ask what is problem of my code for id matching…
always@(posedge aclk)begin
temp = 5;
if(awvalid /*&& awready*/)begin
que.push_back(awid);
que.push_back(awlen+1);
$display("value og q+1",que);
$display("value of que",que.size);
end
for(int i=0;i<que.size();i=i+2)
begin
if(wvalid==1 /*&& wready*/)begin
if(wid == que[i])begin
// $display("----------------------------------value of temp***************************************************");
que[i+1]--;
$display("HEY 2 PRAHSNAT-----------------------------------------------------------------",wvalid,,que[i+1],,i,,wid,,que[i]); $display("QUEUE VALUE IS :",que);
$display("value og q+1",que[i+1]);
temp2=que[i+1];
$display("HEY PRAHSNAT-----------------------------------------------------------------",temp2);
if(que[i+1]==0)begin
temp = que[i+1];
$display("----------------------------------value of temp***************************************************",temp);
que.delete(i);
que.delete(i);
end
end
end
end
end
property p8;
@(aclk)if(temp==0 && aclk==1 && wvalid==1)
##0 wlast ;
endproperty
pass_awlen_eq_wdata:assert property(p8) ;
In reply to prashu:
It’s very hard to answer your question unless one really knows the interface and your design.
However, I can make general comments about your assertion:
Your concurrent assertion seems weak in style in that it does not reflect sequences. Not that it is not wrong to do that, just that your title “master slave for id matching and received data” seem to imply some sort of of a matching of items that occur over a period of time.
Your support code does not seem to reflect support of the assertion
I suggest that you write some concurrent assertions to support what you are trying to verify.
// write response channel signals
input [TXID_BITS - 1:0] bid,
input logic[1:0] bresp,
input bvalid,
input bready);
// int que[$];
int awid_arry[int];
// int temp,temp2;
int b;
always @(posedge aclk)
begin
if( awvalid==1 && awready==1 )
begin
awid_arry[awid] = awlen + 1;
end
end
always @(posedge aclk)
begin
if( wvalid==1 && wready==1 )
begin
if(awid_arry.exists(wid))
begin
if( awid_arry[wid]>0 )begin
awid_arry[wid]–;
b = awid_arry[wid];
$display(“vvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvv”);end
else begin
$error(“id is not valid”);end
end
end
else begin
$error( “not exist”);end
end
sequence s1;
int cnt[int];
@( posedge aclk)
(awvalid && awready ) ##0 (awid_arry[awid] = awlen) ##0 (cnt[awid]++,wvalid)[*0:$] ##0 ( cnt[awid] == awid_arry[awid] );
endsequence
property p1;
##0 s1;
endproperty
ERRRRRRRRRRRRRRRRRRRRRR: assert property(p1);
endmodule
is it week assertion?
plz tell me how we can write assertion for axi master slave
in my code master vip master send awaddr and control information such as awlen per posedge aclk where slave vip received it .same as master send write data and slave received it bt i want to assert on such as if master send awlen=7 after that master send data transfer 8 times then my assertion will shout erro…
and what is the mistake in my sequence block?
In reply to prashu:
Quick reply because I don’t want to get into the protocol or your requirements of your design. However, I’ll give you guidelines based on what I see on your approaches.
An assertion is an expression of your requirements, and it is used to check that the design abides by your requirements.
An assertion is not an expression of the implementation of the design.
your sequence s1 (copied below) is a sequence that lasts ONE clock sample. This is because ##0 is a ZERO clock delay; you probably meant to say ##1
sequence s1; // A poorly written, with errors, sequence used as a property
int cnt[int];
@( posedge aclk)
(awvalid && awready ) ##0 (awid_arry[awid] = awlen)
##0 (cnt[awid]++,wvalid)[*0:$] ##0 ( cnt[awid] == awid_arry[awid] );
endsequence
An assertion of a sequence is generally not recommended because at every clocking event, a new attempt is started and some threads will show failures, though that is not the intent. I explain that in my SVA book.
Concurrent assertions typically have an antecedent and a consequent; when the antecedent does not match, the property is vacuous. For example,
a_new_triggering_sequence |-> an_expected_response_sequence_or_property;
// for example
$rose(req) |-> ##[1:3] sys_ready ##1 ack;
If what I wrote so far is confusing to you, then you really need to study SVA and its applications to verify requirements.