I need to verify that a signal A is not only held low, when power_off is 1,but also held low for n cycles, after power_off transitions to 0, and further, also held low for n cycles before power_off again transitions from a 0 to a 1.
In other words, signal A will be high, only in the time interval of n cycles after power on to n cycles before power off.
In reply to assert_yourself:
Your requirements were ambiguous at first, and your description …n cycles before power_off is confusing. However, if you approach the problem in a forward looking direction, the requirements can easily be translated to SVA.
Below is my code and simulation. I used the pass/fail signals to more easily see when an assertion passes or fails.
https://systemverilog.us/vf/powern.sv // code
Edit code - EDA Playground
module m;
bit clk, p_off, a;
int n=4, pass1, pass2, pass3, pass4, pass5, fail1, fail2, fail3, fail4, fail5;
initial forever #1 clk = !clk;
// p_off +--------+---**-----+--------+
// --------+ +-----------
// <---n---> <---n--->
// a +---**-----+
// ------------------+ +-----------------
// 1) a==0 p_off==1 while number of clocks from $rose(p_off)to $rose(a) == n
// 2) a==0 p_off==1 while number of clocks from $fell(a)to $fell(p_off) == n
// 3) p_off==1 from $rose(p_off) to $fell(a)
// 4) $rose(a) to $fell(a) is within $rose(p_off) to $fell(p_off)
// 5) fell(p_off) then a==0
//
// 1) a==0 p==1 while number of clocks from $rose(p_off)to $rose(a) == n
property p_PtoA;
int v;
@(posedge clk) ($rose(p_off), v=0) |->
(a==0 && p_off==1, v=v+1)[*1:$] ##1 $rose(a) ##0 v==n;
endproperty
ap_PtoA: assert property(p_PtoA) pass1=1; else fail1=1;
// 2) a==0 p_off==1 while number of clocks from $fell(a)to $fell(p_off) == n
property p_A0toP1;
int v;
@(posedge clk) ($fell(a), v=0) |->
(a==0 && p_off==1, v=v+1)[*1:$] ##1 $fell(p_off) ##0 v==n;
endproperty
ap_P0toA1: assert property(p_A0toP1) pass2=1; else fail2=1;;
// 3) p_off==1 from $rose(p_off) to $fell(a)+1
ap_poff_toa0: assert property(@(posedge clk) $rose(p_off) |->
p_off[*1:$] ##0 $fell(a)) pass3=1; else fail3=1;
// 4) $rose(a) to $fell(a) is within $rose(p_off) $fell(p_off)
ap_a_within: assert property(@(posedge clk) $rose(p_off) |->
$rose(a) ##[1:$] $fell(a) within 1 ##[1:$] $fell(p_off)) pass4=1; else fail4=1;
// 5) fell(p_off) then a==0
ap_poff_0a0: assert property(@(posedge clk) $fell(p_off) |-> a==0) pass5=1; else fail5=1;
initial begin
$dumpfile("dump.vcd"); $dumpvars;
@(posedge clk) p_off<=1;
repeat(4) @(posedge clk);
a <=1;
repeat(6) @(posedge clk);
a<=0;
repeat(4) @(posedge clk);
p_off <=0;
#20 $finish;
end
endmodule
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
Thanks a lot, Ben. Your guidance is really valuable to me.
In reply to assert_yourself:
