// length value will change dynamically, len is signal
// READ_DATA = 32;
// tag is some value.
for(genvar i = 0; i <= (length/(READ_DATA/8)); i++) begin
property_a: assert property (P_TAG_CHECK(tag))
else $error("ERROR");
end
I am using this genvar approach, it is throwing error(Because of dynamic variable) any work around for that (or) any other approach for this scenario.
My intension is to generate assert properties based on the condition of length/(DATA_WIDTH/8).
In reply to Pavan Kumar Kollipara:
The easiest way to use dynamic variables in SVA is to use my package:
SVA Package: Dynamic and range delays and repeats SVA: Package for dynamic and range delays and repeats | Verification Academy
The file includes a testbench.
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
…
Hello Ben,
Thanks for your reply,
// length value will change dynamically, len is signal
// READ_DATA = 32;
// tag is some value
sequence STS_AND_TAG_CHECK(tag);
@(posedge rd_rsp_clk) disable iff (rst_n !== 1)
rdata_valid |-> ((rdata_tag == tag) && (wr_rsp_error == 0 || wr_rsp_error == 1));
endsequence: STS_AND_TAG_CHECK
//----------------------------------------------------------------
// ****** DYNAMIC REPEAT q_s[*d1] **********
// Application: $rose(a) |-> q_dynamic_repeat(q_s, d1) ##1 STS_AND_TAG_CHECK;
sequence q_dynamic_repeat(count);
int v=count;
(1, v=count) ##0 first_match((1, v=v-1'b1) [*1:$] ##0 v<=0);
endsequence
A_STS_AND_TAG: assert property ($rose(cmd_valid) |-> q_dynamic_repeat(cmd_len/(READ_DATA/8)) ##0 STS_AND_TAG_CHECK(cmd_tag))
else $error("ERROR");
please let me know it is correct or not.
Hello Ben,
This is the assertion I have written previously,
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));
endproperty: P_TAG_CHECK
// length(signal) is the signal changes with every command valid
// parameter READ_DATA = 32;
// tag is some value
always @(posedge cmd_valid) begin
if(cmd_type == 0 && cmd_last == 1) begin
for(genvar i = 0; i <= (length/(READ_DATA/8)); i++) begin
property_a: assert property (P_TAG_CHECK(tag))
else $error("ERROR");
end
end
end
I am using this genvar approach, it is throwing error(Because of dynamic variable) any work around for that (or) any other approach for this scenario.
My intension is to generate assert properties based on the condition of length/(DATA_WIDTH/8).
Thanks,
Pavan.
In reply to Pavan Kumar Kollipara:
I don’t understand your assertion.
My intension is to generate assert properties based on the condition of length/(DATA_WIDTH/8).
So you want to dynamically start (or fire) a number of assertions based on a value of a variable. I generally have used the genvar in the generate construct. The following should work:
always @(posedge cmd_valid) begin
if(cmd_type == 0 && cmd_last == 1) begin
for(int i = 0; i <= (length/(READ_DATA/8)); i++) begin
property_a: assert property (P_TAG_CHECK(tag))
else $error("ERROR");
end
end
end
But I don’t understand why you need to create multiple identical assertions. Specifically,
assuming that at time t (length/(READ_DATA/8))== 3, this for loop create 3 identical assertions that are initated at @(posedge rd_rsp_clk) and last 1 cycle. The value of “tag” is identical for all 3, and “tag” does not depend on the iteration loop “i”. If you had something like P_TAG_CHECK(tag * i), then I can perhaps see some value to the multiple separate assertions. What you wrote could be simplified without the for loop.
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
…
Hello Ben,
Thanks for your reply,
Here length and tag value changes with the cmd_valid, for every cmd_valid those both tag and length values will change.
I have used previously by keeping only for loop, I am getting Below error
always @(posedge cmd_valid) begin
if(cmd_type == 0 && cmd_last == 1) begin
for(int i = 0; i <= (length/(READ_DATA/8)); i++) begin
property_a: assert property (P_TAG_CHECK(tag))
else $error("ERROR");
end
end
end
Error-[V2KGEUV] Unknown or bad value for genvar
/src/assertions/mim_bfm_assertions.sv, 659
Instance/Generate block name: test_tb.tes_if.u_test_assert
Elaboration time unknown or bad value encountered for generate for-statement
condition expression.
Please make sure it is elaboration time constant.
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*==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:
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
…
Thanks Ben for your detailed explanation, I have understood the problem and will modify code according to the perfect scenario
Ben – take a look at my paper Understanding the SVA Engine, you may want to use that approach if that is simpler for you.
I will go thorough this paper once.
Thanks,
Pavan.