There are 4 signals req,ack,data and data_wait. when req is sent, we receive ack,after that data will be sent. when data_wait is LOW ,data is sampled and when HIGH, data will not be sampled how to write assertion for this condition?
I have been asked to write the above one in asseertion and can you help me in it.
and also I have one doubt:
proprty clk_test;
a&b-> if() ---->why we cannot write if condition after the enabling conditions?
regards
Raghu
In reply to raghunalla:
Other than “when req is active, ack should eventually become active”, the rest of your requirements are not clear. What does it mean to send data and how would we know when it is sampled?
What are you trying to achieve with an if condition? An action block may be what you want.
In reply to dave_59:
In reply to raghunalla:
Other than “when req is active, ack should eventually become active”, the rest of your requirements are not clear. What does it mean to send data and how would we know when it is sampled?
What are you trying to achieve with an if condition? An action block may be what you want.
sampling in the sense the data should not be zero.
when data_wait=LOW the data should not be equal to zero and when data_wait is HIGH the data should either zero or unknown.
property abc;
a=> if(condition)b else c;
endproperty
can we write this kind of assertion?
In reply to raghunalla:
Write multiple small assertions
// There are 4 signals req,ack,data and data_wait.
// when req is sent, we receive ack,
// after that data will be sent.
// when data_wait is LOW ,data is sampled and
// when HIGH, data will not be sampled how to write assertion for this condition?
// when data_wait=LOW the data should not be equal to zero and
// when data_wait is HIGH the data should either zero or unknown.
ap_req_ack: assert property(@(posedge clk) $rose(req) |-> ack[->1]);
ap_ack2data: assert property(@(posedge clk) $rose(ack) |->
data_wait==1[->1] ##1 data_wait==0[->1]);
ap_datawait1: assert property((data_wait==1 |-> data==0 || data=='X));
ap_datawait0: assert property((data_wait==0 |-> data!=0 && data!='X));
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
…
Udemy courses by Srinivasan Venkataramanan (http://cvcblr.com/home.html)
https://www.udemy.com/course/sva-basic/
https://www.udemy.com/course/sv-pre-uvm/
In reply to peter:
That’s a new requirement.
On the missed the posedge clock, you can use the default clocking to avoid writing it.
// how about ack can not be self asserted,unless
// request is asserted before. How to modify ap_req_ack?
default clocking @(posedge clk);
endclocking
bit req_occur;
always_ff @(posedge clk) begin: req_latch
if(req && !ack) req_occur <= 1;
if(ack && !req) req_occur <= 0;
end: req_latch
ap_ackreq: assert property($rose(ack) |-> req_occur);