In reply to Pavan Kumar Kollipara:
I still don't understand why you need a loop. Typically, in assertions, you may want to use the generate statement to instantiate multiple assertions based on the the genvar variable. For example:
module arbiter;
//If I have to test a arbiter encoded arbiter with say, 4-inputs (request signals) and 4-outputs (grant signals),
//What assertions are required for verifying this arbiter?
bit[15:0] req, grnt;
bit clk;
initial forever #5 clk=!clk;
generate for (genvar i=0; i<=15; i++)
begin
property p_arbiter;
bit[16:0] v;
(req[i]==1'b1, v=0, v[i+1]=1'b1) ##0 req < v |->
grnt[i]==1'b1 ##0 $onehot(grnt);
endproperty : p_arbiter
ap_arbiter: assert property(@(posedge clk) p_arbiter);
end
endgenerate
endmodule
In your model, I believe that you need to put the conditions to do the verification in the antecendent. Before getting into it, I am puzzled by the expression
(rdata_error == 0 || rdata_error == 1))
Unless rdata_error is a vector and can have other values, the expr && (bit_a==0 || bit_a==1) is equivalent to expr.
property P_TAG_CHECK(tag);
@(posedge rd_rsp_clk) disable iff (rst_n !== 1)
rdata_valid ##0 ((rdata_tag == tag) &&
(rdata_error == 0 || rdata_error == 1)); // rdata_error is NOT a bit
endproperty: P_TAG_CHECK
p_a: assert property(@(posedge cmd_valid)
cmd_type == 0 && cmd_last == 1) |-> P_TAG_CHECK(tag))
else $error("ERROR");
Comments:
- Why are you using 2 clock systems: (posedge cmd_valid) and (posedge rd_rsp_clk).
Remember that the variables are sampled in the Preponed Region. @(posedge cmd_valid) cmd_type is sampled just before the event (posedge cmd_valid).
- You can use the generate endgenerate, this is expanded at elaboration and not during simulation.
- rethink your model. I don't believe that you fully understand the requirements because you are having a very hard time expressing them in a verification language.
- take a look at my paper Understanding the SVA Engine,, you may want to use that approach if that is simpler for you.
https://verificationacademy.com/verification-horizons/july-2020-volume-16-issue-2
Ben Cohen
http://www.systemverilog.us/
For training, consulting, services: contact
http://cvcblr.com/home
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
...
1) SVA Package: Dynamic and range delays and repeats https://rb.gy/a89jlh
2) Free books: Component Design by Example https://rb.gy/9tcbhl
Real Chip Design and Verification Using Verilog and VHDL($3) https://rb.gy/cwy7nb
3) Papers:
- SVA Alternative for Complex Assertions
https://verificationacademy.com/news/verification-horizons-march-2018-issue
- SVA in a UVM Class-based Environment
https://verificationacademy.com/verification-horizons/february-2013-volume-9-issue-1/SVA-in-a-UVM-Class-based-Environment
- Understanding the SVA Engine,
https://verificationacademy.com/verification-horizons/july-2020-volume-16-issue-2