Hello all,
I was working on AXI, I want to verify the transaction ID in a write transfer. I have written an assertion to verify this.
I am facing an issue with it.
sequence addr_syn;
(S_AXI_AWREADY && S_AXI_AWVALID);
endsequence
sequence data_syn;
(S_AXI_WREADY && S_AXI_WVALID);
endsequence
sequence resp_syn;
(S_AXI_BVALID && S_AXI_BREADY);
endsequence
property axi_id_check;
// @(posedge clk);
int loc_awid;
int loc_awlen;
int loc_wid[bit];
int loc_bid;
(addr_syn,loc_awid = S_AXI_AWID,loc_awlen = S_AXI_AWLEN)
//Getting the AWID and AWLEN
##[0:$]((data_syn and loc_awlen),loc_wid[S_AXI_WID] = S_AXI_WID,loc_awlen=loc_awlen-1)
// Getting all WID of write data
|=>(resp_syn,loc_bid = S_AXI_BID) ##0 id_check(loc_awid,loc_wid,loc_bid);
//Getting respones ID BID.
endproperty
function bit id_check();
input int loc_awid;
input int loc_wid[bit];
input int loc_bid;
begin
foreach(loc_wid[i])
begin
if(loc_wid[i] != loc_awid != loc_bid)
$display("ID is matched mismatch AWID:-%0d,WID:-%0d,BID:-%0d",loc_awid,loc_wid[i],loc_bid);
else
$display("ID is matched matched AWID:-%0d,WID:-%0d,BID:-%0d",loc_awid,loc_wid[i],loc_bid);
end
return 1;
end
endfunction
A1:assert property(axi_id_check);
I was trying to get all ID values and passing to the values into a function. but, end with an error message.
Error-[ETTNATE] Invalid type in temporal expression
" Expressions involving real, string, event, tagged union and dynamic
SystemVerilog types are not allowed in Boolean expressions in properties and
sequences.
Source info: loc_wid[S_AXI_WID] = S_AXI_WID; "
My doubt is Can an array be used inside a property to get the value? or Is there any other way to get all values and compare.?
In reply to SriGanesh D:
A few errors + a recommendation:
(data_syn and loc_awlen) // ERROR
// *** “and” is a sequential operator, you need &&
Expression defined as a sequence
No need to do this, particularly since there are different rules for sequences and expressions. Use the let instead
Antecedent is multithreaded, limit to one match
An antecedent with multiple threads requires ALL threads to be tested for a success.
Use the first_match() or the goto operator
property p;
bit x;
w ##1 (a, x=1)[->1] |-> b; // goto is preferred for style, first_match() is OK though
endproperty
// <--------------------The fix ---------------------------------->
let addr_syn=(S_AXI_AWREADY && S_AXI_AWVALID);
let data_syn=(S_AXI_WREADY && S_AXI_WVALID);
let resp_syn=(S_AXI_BVALID && S_AXI_BREADY);
property axi_id_check;
// @(posedge clk);
int loc_awid;
int loc_awlen;
int loc_wid[bit];
int loc_bid;
(addr_syn, loc_awid = S_AXI_AWID, loc_awlen = S_AXI_AWLEN)
//Getting the AWID and AWLEN
first_match(##[0:$]((data_syn && loc_awlen), loc_wid[S_AXI_WID] = S_AXI_WID, loc_awlen=loc_awlen-1))
// Getting all WID of write data
|=>(resp_syn, loc_bid = S_AXI_BID) ##0 id_check(loc_awid,loc_wid,loc_bid);
//Getting respones ID BID.
endproperty
//..
A1:assert property(axi_id_check);
Hello Ben
Thanks for the response. Could you please explain about “antecedent is multithreaded, limit to one match”? I am really confused about this concept.