Hi,
I need to write assertions for timing registers ex:
reg [3:0] thv_count;
thv_count = (23*clk_period);
Assertion: assert property(@(posedge clk)) ($rose(FLASH.prog) && (rose(FLASH.erase)) |-> ##[thv_count : ] ($rose(FLASH.nvstr));
clk_period keeps changing.
For the above code i am getting an error as illegal operand for constant expression. i cannot use reg value at constant expression. please let me know how to solve the error.
This should work:
module clk_period;
logic [3:0] thv_count;
int clk_period=10;
bit clk;
default clocking cb_ck1 @ (posedge(clk)); endclocking
initial forever #10 clk=!clk;
assign thv_count = (23*clk_period);
// assert property(@(posedge clk)) ($rose(FLASH.prog) && ($rose(FLASH.erase)) |->
// ##[thv_count : $] ($rose(FLASH.nvstr));
property p_flash;
logic [3:0] v_thv_count;
($rose(FLASH.prog) && ($rose(FLASH.erase)), v_thv_count=0) |=>
(1, v_thv_count=v_thv_count+1'b1)[*1:$] ##1 v_thv_count==thv_count // get to thv_count
##[0:$] ($rose(FLASH.nvstr)); // changed from ##[1:$]
endmodule
Ben Cohen, Design and verification expert (310) 997-2187
http://www.systemverilog.us/ ben@systemverilog.us
In reply to ben@SystemVerilog.us:
Note: If the value of thv_count changes during the assertion, and one needs to capture the value of that variable during a nonvacuous attempt, then you would need to save the value of that variable into a local variable. Thus,
module clk_period;
logic [3:0] thv_count;
int clk_period=10;
bit clk;
default clocking cb_ck1 @ (posedge(clk)); endclocking
initial forever #10 clk=!clk;
assign thv_count = (23*clk_period);
// assert property(@(posedge clk)) ($rose(FLASH.prog) && ($rose(FLASH.erase)) |->
// ##[thv_count : $] ($rose(FLASH.nvstr));
property p_flash;
logic [3:0] v_thv_count, v_count_hold;
($rose(FLASH.prog) && ($rose(FLASH.erase)), v_thv_count=0, v_count_hold=thv_count) |=>
(1, v_thv_count=v_thv_count+1'b1)[*1:$] ##1 v_thv_count==v_count_hold // get to thv_count
##[0:$] ($rose(FLASH.nvstr)); // changed from ##[1:$]
endmodule
Ben Cohen, Design and verification expert (310) 997-2187
http://www.systemverilog.us/ ben@systemverilog.us
In reply to ben@SystemVerilog.us:
Hi Ben,
Thanks for replying to the query,
property a4;
logic [15:0] v_Tnvh_count;
@(posedge clk)(fell(FLASH.erase), v_Tnvh_count=0) |=> (1, v_Tnvh_count=v_Tnvh_count+1'b1)[*1:] ##1 (v_Tnvh_count == Tnvh_count) ##[1:$] ($fell(FLASH.nvstr));
endproperty : a4
Assertion4: assert property (a4);
problem here is this assertions is getting activated at every posedge of clk and waiting for $fell(FLASH.erase) event, but this event occurs only once, assertion finishes and gets activated again in the next clk cycle, hence assertion is failing. how do i avoid un necessary failing of assertion
In reply to sahmed01:
problem here is this assertions is getting activated at every posedge of clk and waiting for $fell(FLASH.erase) event, but this event occurs only once, assertion finishes and gets activated again in the next clk cycle, hence assertion is failing. how do i avoid un necessary failing of assertion
I am not totally clear on your issue. Perhaps the following will clarify things:
Ben Cohen, Design and verification expert (310) 997-2187
http://www.systemverilog.us/
If it is desired to fire one assertion that has a true antecedent until its outcome is determined, you can use a semaphore. Below is an example of this base on your model.
Note tha in this model the assertion can never fail because of the ##[1:$]
module clk_period;
logic [3:0] thv_count;
int clk_period=10;
bit clk, flag;
default clocking cb_ck1 @ (posedge(clk)); endclocking
initial forever #10 clk=!clk;
assign thv_count = (23*clk_period);
// Semaphore
function void set_flag();
flag=1'b1;
endfunction : set_flag
// assert property(@(posedge clk)) ($rose(FLASH.prog) && ($rose(FLASH.erase)) |->
// ##[thv_count : $] ($rose(FLASH.nvstr));
property p_flash;
logic [3:0] v_thv_count;
(!flag && $rose(FLASH.prog) && ($rose(FLASH.erase)), v_thv_count=0, set_flag()) |=>
(1, v_thv_count=v_thv_count+1'b1)[*1:$] ##1 v_thv_count==thv_count // get to thv_count
##[1:$] ($rose(FLASH.nvstr));
endproperty
ap_flash: assert property( p_flash) flag<=1'b0;
endmodule
Hi,
I am getting this error, what does it mean and wat do i do
@(posedge clk)(($stable(YADR) && stable(DIN)), v_Tads_count=0) |=> (1, v_Tads_count = v_Tads_count+1'b1)[*1:] ##1 v_Tads_count == Tads_count ##[1:$] ($rose(YE));
|
ncsim: *E,ASRTST (…/tb_top/assertions.sva,180): (time 8115680 PS) Assertion top_tb.t1.Assertion13 has failed (182 cycles, starting 0 FS)
Please help
In reply to sahmed01:
Your assertion should never fail because of ##[1:]. It can either be vacuous if the antecedent is false, or it can succeed if the consequent is true. Below is a modified code that models the structure of what you have (I used "a" and "b" to reflect your expressions. Try this code in ncsim. Questa showed a single success at 2050ns Also try different variations, like (1, v_count=v_count+1)[*1:] ##1 v_count==count; // ##[1:$] b;
module rep0;
bit clk, a=0, b=0;
int count;
default clocking cb_ck1 @ (posedge(clk)); endclocking
initial forever #10 clk=!clk;
// @(posedge clk)(($stable(YADR) && $stable(DIN)), v_Tads_count=0) |=>
// (1, v_Tads_count = v_Tads_count+1'b1)[*1:$] ##1 v_Tads_count == Tads_count ##[1:$] ($rose(YE));
property p_count;
int v_count;
($rose(a), v_count=0) |=>
(1, v_count=v_count+1)[*1:$] ##1 v_count==count ##[1:$] b;
endproperty : p_count
ap_count : assert property(p_count);
initial begin
repeat (2) @ (posedge clk);
a <= 1'b1;
count <= 5;
repeat(100) @ (posedge clk);
b <= 1'b1;
end
endmodule : rep0
Ben Cohen, Design and verification expert (310) 997-2187
http://www.systemverilog.us/ ben@systemverilog.us
Ben,
property a9;
int v_Twpr_count;
($fell(YE) && $fell(SE) && fell(NVSTR),v_Twpr_count=0) |=> (1, v_Twpr_count = v_Twpr_count+1)[*1:] ##1 v_Twpr_count == Twpr_count ##[1:$] ($rose(ERASE) || $rose(PROG));
endproperty : a9
Assertion9 : assert property(a9);
for the above code, assertions are getting activated on the 1st clk tick itself, but the actual scenario i need to check is: as soon as YE, SE and NVSTR goes low, need to wait for minimum Twpr_count system clk cycles before program or erase operation take place. How do i avoid this from happening.
(AT 0 simulation time all register values are zero)
In reply to sahmed01:
Code below will do the trick. Fire the assertion after the desired number of clocks.
Key here is this
initial begin
repeat (Twpr_count) @ (posedge clk);
go <= 1'b1; // flag for debug, not needed otherwise
forever @ (posedge clk) Assertion9 : assert property(a9);
end
Test code
module testset;
bit clk, go, YE, SE, NVSTR, ERASE, PROG;
int Twpr_count=16;
default clocking cb_clk @ (posedge clk); endclocking
initial forever #10 clk=!clk;
property a9;
int v_Twpr_count;
($fell(YE) && $fell(SE) && $fell(NVSTR),v_Twpr_count=0) |=>
(1, v_Twpr_count = v_Twpr_count+1)[*1:$] ##1 v_Twpr_count == Twpr_count ##[1:$] ($rose(ERASE) || $rose(PROG));
endproperty : a9
initial begin
repeat (Twpr_count) @ (posedge clk);
go <= 1'b1;
forever @ (posedge clk) Assertion9 : assert property(a9);
end
always @ (posedge clk) begin : aly
#2 if(!randomize(YE, SE, NVSTR, ERASE, PROG)) $error("randomization failure");
end : aly
//for the above code, assertions are getting activated on the 1st clk tick itself,
// but the actual scenario i need to check is: as soon as YE, SE and NVSTR goes low,
// need to wait for minimum Twpr_count system clk cycles before program or erase operation take place.
// How do i avoid this from happening.
//(AT 0 simulation time all register values are zero)
endmodule : testset
Ben Cohen, Design and verification expert (310) 997-2187
http://www.systemverilog.us/ ben@systemverilog.us
repeat (Twpr_count) @(posedge clk);
|
ncvlog: *E,SFLPIN (…/tb_top/assertions.sva,180|13): Procedural code in initial block containing concurrent assertions.
property a9;
int v_Twpr_count;
($fell(YE) && $fell(SE) && fell(NVSTR),v_Twpr_count=0) |=> (1, v_Twpr_count = v_Twpr_count+1)[*1:] ##1 v_Twpr_count == Twpr_count ##[1:$] ($rose(ERASE) || $rose(PROG));
endproperty : a9
bit go;
initial begin
repeat (Twpr_count) @(posedge clk);
go <= 1’b1;
forever @(posedge clk) Assertion9 : assert property(a9);
end
in the above code Assertion9 is triggered after Twpr_count ? If yes then this will not serve our purpose right. what if YE SE and NVSTR signal goes low during Twpr_count, will that be not missed. please clarify.
thanks
In reply to sahmed01:
Two issues:
repeat (Twpr_count) @(posedge clk);
|
ncvlog: *E,SFLPIN (../tb_top/assertions.sva,180|13): Procedural code in initial block containing concurrent assertions.
property a9;
int v_Twpr_count;
($fell(YE) && $fell(SE) && $fell(NVSTR),v_Twpr_count=0) |=> (1, v_Twpr_count = v_Twpr_count+1)[*1:$] ##1 v_Twpr_count == Twpr_count ##[1:$] ($rose(ERASE) || $rose(PROG));
endproperty : a9
Assertion9 : assert property(a9);
If the simulator thinks that there is a $fell at time 0 then your simulator is in error.
However, for your case, you could simply change the repeat to 1 cycle. Thus,
initial begin
repeat (1) @(posedge clk); // or simply @(posedge clk);
go <= 1'b1;
forever @(posedge clk) Assertion9 : assert property(a9);
end
Ben Cohen systemverilog.us
In reply to ben@SystemVerilog.us:
If initial gives you trouble (this is an NcSim issue if it is), then do the following:
bit start;
always @ (posedge clk) begin
if (!start) start <= 1'b1;
else Assertion9 : assert property(a9);
end
Ben Cohen systemverilog.us
Still it is pointing error, if it is simulator error, what do i do? how do i avoid this?
property a9;
int v_Twpr_count;
($fell(YE) && $fell(SE) && fell(NVSTR),v_Twpr_count=0) |=> (1, v_Twpr_count = v_Twpr_count+1)[*1:] ##1 v_Twpr_count == Twpr_count ##[1:$] ($rose(ERASE) || $rose(PROG));
endproperty : a9
bit start;
always @ (posedge clk) begin
if (!start) start <= 1’b1;
else Assertion9 : assert property(a9);
end
ERROR:
if (!start) start <= 1’b1;
|
ncvlog: *E,SFLPCN (…/tb_top/assertions.sva,191|4): Procedural code in always block containing concurrent assertions.
In reply to sahmed01:
bit start;
always @ (posedge clk) begin
if (!start) start <= 1’b1;
else Assertion9 : assert property(a9);
end
ERROR:
if (!start) start <= 1’b1;
|
ncvlog: *E,SFLPCN (…/tb_top/assertions.sva,191|4): Procedural code in always block containing concurrent assertions.
Going back to SystemVerilog 3,1 (in 2003)
17.12 Concurrent assertions
A property on its own is never evaluated for checking an expression. It must be used within a verification statement for this to occur. A verification statement states the verification function to be performed on the property. The statement can be one of the following:
— assert to specify the property as a checker to ensure that the property holds for the design
— cover to monitor the property evaluation for coverage
A concurrent assertion statement can be specified in:
— an always block or initial block as a statement, wherever these blocks can appear
— a module as a module_or_generate_item
— an interface as an interface_or_generate_item
— a program as a non_port_program_item
— $root
You need to talk to Cadence as to why they have not supported this SVA requirement. This is not even 2009 feature! It’s a 2003 feature.
Ben Cohen SystemVerilog.us
In reply to ben@SystemVerilog.us:
Since NcSim is giving you grief with procedural concurrent assertion, you could, in some circumstances, have procedural code to write flags that can be used by concurrent (non-procedural) assertions. Thus, for the above problem:
bit start;
always @ (posedge clk) begin
if (!start) start <= 1'b1;
end
else Assertion9 : assert property(start |-> a9);
However, one would lose a lot of capabilities in not being able to write procedural concurrent assertions.
Ben Cohen http://www.systemverilog.us/
In reply to ben@SystemVerilog.us:
I did an inquiry with Cadence and it looks like NcSim does support procedural concurrent assertions. A response: "If your question is for concurrent assertions in procedural block, its supported in ncsim. One has to us a (compile-time) switch –procsva ".
Ben systemverilog.us
property a3;
reg [15:0] v_Tnvs_count;
(rose(ERASE),v_Tnvs_count=0) |=> (1, v_Tnvs_count = v_Tnvs_count+1'b1)[*1:] ##1 (v_Tnvs_count == Tnvs_count) ##[1:$] ($rose(NVSTR));
endproperty : a3
Assertion3 : assert property (a3);
how can i add V_Tnvs_count to simvision. I want to see how this signals will behave at each clk
Thanks-
As the scope of the signal is within the property, how do i dump that signal into simvision?
Thanks-
In reply to sahmed01:
As the scope of the signal is within the property, how do i dump that signal into simvision?
Viewing the local variables of a property is a function of the debugging tools, and is vendor dependent. I have Questa, and with Questa one can use the Assertion Thread Viewer (ATV) that provides the values of the local variables. I have not used NcSim for a long time.
Ben SystemVerilog.us