How to implement the following check through assertions:
When the en signal is pulled low, the clk can still jump normally for a maximum of 3 times, and then it must be turned off, that is, it should remain unchanged.
// When the en signal is pulled low, the clk can still jump normally for
// a maximum of 3 times, and then it must be turned off,
// that is, it should remain unchanged.
// Two approaches:
// 1) Using a task that can be called without a running other tb clock
task automatic t_clk_en0();
int count;
fork
#10; // 5 clks
forever @(posedge clk) if((!en) count=count+1;
join_any
am_3clk_after_en: assert(count < 3) else err=err+1;
endtask
always @(!en) t_clk_en0();
// or called with a running other clock
cover property(@(posedge clk_tb) !en |-> (1, t_clk_en0()));
// 2) An assertion using a running tb clock
// Using the tb clock
property p_noclk_en; // adjust the max count allowed
int count=0;
@(posedge clk_tb) $fell(en) |-> ##1
(1, count=count+1)[*1:$] ##0 count<4 intersect $rose(en)[->1];
endproperty
ap_noclk_en: assert property(p_noclk_en) else err1=err1+1;
module top2;
bit clk, en=1, en1=1, clk_tb;
int err, err1;
always #1 clk_tb=!clk_tb;
always_comb clk = clk_tb && en1;
always en1 = #10 en;
// When the en signal is pulled low, the clk can still jump normally for
// a maximum of 3 times, and then it must be turned off,
// that is, it should remain unchanged.
task automatic t_clk_en0();
int count;
fork
#10; // 5 clks
forever @(posedge clk) if((!en) count=count+1;
join_any
am_3clk_after_en: assert(count < 3) else err=err+1;
endtask
// fire the task
// cover property(@(posedge clk_tb) !en |-> (1, t_clk_en0()));
always @(!en) t_clk_en0();
// Using the tb clock
property p_noclk_en; // adjust the max count allowed
int count=0;
@(posedge clk_tb) $fell(en) |-> ##1
(1, count=count+1, count=count+1)[*1:$] ##0 count<4 intersect $rose(en)[->1];
endproperty
ap_noclk_en: assert property(p_noclk_en) else err1=err1+1;
initial begin
$dumpfile("dump.vcd"); $dumpvars;
#10 en=0;
#25 en=1;
#30 en=0;
#50 en=1;
#30; $finish();
end
endmodule
Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.
In reply to ben@SystemVerilog.us:
Hi Ben,
I have a minor qualm here. I saw that in the condition checking term/part ( I don’t know whether this is the proper technical term) You have written count=count+1 twice.
Could you tell me why?
Another question regarding the same is whether we can add more than one condition by using “,” or use logical operators only in that case.
In reply to Shubhabrata:
In reply to ben@SystemVerilog.us:
Hi Ben,
I have a minor qualm here. I saw that in the condition checking term/part ( I don’t know whether this is the proper technical term) You have written count=count+1 twice.
Could you tell me why?
That was an error on my part, apologies.
Another question regarding the same is whether we can add more than one condition by using “,” or use logical operators only in that case.
1800 defines one of the possible way to define a sequence as:
sequence_instance [ sequence_abbrev ] | ( sequence_expr {, sequence_match_item } ) [ sequence_abbrev ]
//Thus,
a ##1 (b, v1=state, v2=0, function_f1(v1, c), v3=f2(), task_k1())[*2]// is all legal
// Of course, a task does not return a value, and it should be automatic
assert property(@(!en) (1, t_clk_en0()));
How to interpret or read this line in assertion ?
(1, count=count+1, count=count+1)[*1:$] ##0 count<4 intersect $rose(en)[->1];
In reply to MP:
// I made a mistake, probably a copy/paste error
(1, count=count+1, count=count+1)[*1:$] ##0 count<4 intersect $rose(en)[->1];
// Should have been
(1, count=count+1)[*1:$] ##0 count<4 intersect $rose(en)[->1];
(1, count=count+1, count=count+1)[*1:$] // is equivalent to
(1, count=count+2)[*1:$]
// My apologies
Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.
or Cohen_Links_to_papers_books - Google Docs
Getting started with verification with SystemVerilog
In reply to ben@SystemVerilog.us:
Hi Ben ,
Have 2 questions related to 2nd approach .
(1) What is the LHS for the intersect operator ?
Is it the sequence : *(1, count=count+1)[1:$] ##0 count<4 OR Only count < 4 ?
I could **replace intersect with throughout** if it were the latter as LHS can't be sequence for throughout.
(2) In your code the local variable is incremented on posedge of clk_tb .
What if I wanted to increment it only when clk toggles and then use clk_tb for intersect operator ?
property p_noclk_en;
int count=0;
@(posedge clk_tb) $fell(en) |=> @( clk ) (1, count=count+1)[*1:$] ##0 @(posedge clk_tb) count<4 intersect $rose(en)[->1];
endproperty
Would this be a correct approach ?
In reply to Have_A_Doubt:
In reply to ben@SystemVerilog.us:
Have 2 questions related to 2nd approach .
(1) What is the LHS for the intersect operator ?
Is it the sequence : *(1, count=count+1)[1:$] ##0 count<4 OR Only count < 4 ?
with
(1, count=count+1)[*1:$] ##0 count<4 intersect rose(en)[->1];
the LHS is
(1, count=count+1)[*1:] ##0 count<4
You can put parentheses if you want; thus,
((1, count=count+1)[*1:$] ##0 count<4) intersect $rose(en)[->1];
I could replace intersect with throughout if it were the latter as LHS can’t be sequence for throughout.
See my paper Reflections on Users’ Experiences with SVA, Part II
Throughout
The syntax for this sequence is: expression_or_dist throughout sequence_expr. The throughout operator specifies that a signal (expression) must hold throughout a sequence. ( b throughout R ) is equivalent to ( b [*0:] intersect R )
((1, count=count+1)[*1:] ##0 count<4) is NOT an expression, but a sequence.
(2) In your code the local variable is incremented on posedge of clk_tb .
What if I wanted to increment it only when clk toggles and then use clk_tb for intersect operator ?
property p_noclk_en;
int count=0;
@(posedge clk_tb) $fell(en) |=> @( clk ) (1, count=count+1)[*1:$] ##0 @(posedge clk_tb) count<4 intersect $rose(en)[->1];
endproperty
Would this be a correct approach ?
The issues are:
(5) - EDA Playground
With **intersect $rose(en)[->1];
**// * Error: (vsim-3937) Asserting on an illegal multiply clocked temporal expression.
// The clock flow cannot change in the RHS of 'intersect' operator.
//------------------------------------
// with **intersect @(posedge clk_tb) $rose(en)[->1];**
property p_noclk_en2; // adjust the max count allowed
int count=0;
@(posedge clk_tb) $fell(en) |=> (@( clk ) (1, count=count+1)[*1:$] ##0 @(posedge clk_tb) count<4) intersect @(posedge clk_tb) $rose(en)[->1];
endproperty
ap_noclk_en2: assert property(p_noclk_en2) else err2=err2+1;
// * Error: (vsim-3937) Asserting on an illegal multiply clocked temporal expression.
// The clock flow cannot change in the RHS of 'intersect' operator.
# // Time: 0 ns Iteration: 0 Instance: /top2 File: testbench.sv Line: 28
Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.
or Cohen_Links_to_papers_books - Google Docs
Getting started with verification with SystemVerilog
This is a better solution to a similar problem:
Requirements: When the en signal is pulled low, the clk_gated can still jump normally for a maximum of 3 times, and then it must be turned off, that is, it should remain unchanged. There is a clk_ref that generates the clk_gated; it runs at twice the frequency of the clk_gated.
//The assertion, using task and immediate assertion
bit clk_gated, clk_ref, en=1, en1=1;
int pass, pass2, err, err2, tbcount;
always #1 clk_ref=!clk_ref;
always_comb clk_gated = clk_ref && en1;
always en1 = #4 en;
// When the en signal is pulled low, the clk_gated can still jump normally for
// a maximum of 3 times, and then it must be turned off,
// that is, it should remain unchanged.
task automatic t_clk_en0();
int count;
fork
#10; // 5 clk_gateds
forever @(posedge clk_gated) if(!en) begin
count=count+1;
tbcount=count; // debug
end
join_any
am_3clk_after_en: assert(count <= 3) pass2++; else err2=err2+1;
endtask
// fire the task
// cover property(@(posedge clk_ref) !en |-> (1, t_clk_en0()));
always @(negedge(en)) t_clk_en0();
// Using the tb clock
property p_noclk_en; // adjust the max count allowed
int count=0;
@(posedge clk_ref) $fell(en) |-> ##1
((1, count=count+clk_gated)[*1:$] intersect $rose(en)[->1]) ##0 count<=3 ;
endproperty
ap_noclk_en: assert property(p_noclk_en) pass++; else err=err+1;