Hi,
I have a CLK and A signal as shown in the figure. When A signal is triggered, I need to make sure that the clock is not running before and after for 1us.
I also have a reference clock in higher frequency that is always running. How can I achieve this requirement using SystemVerilog assertion?
Thanks
SVA does not work well for requirements like these.
What works best is SV and automatic tasks forked by a condition. There, local variables are visible by all elements of the forks. This is unlike SVA where local variables in AND OR sequences or properties are not shared.
Let me know if that works out for you.
/* I have a CLK and A signal as shown in the figure. When A signal is triggered,
I need to make sure that the clock is not running before and after for 1us.
I also have a reference clock in higher frequency that is always running.
How can I achieve this requirement using SystemVerilog assertion? */
// +---+ +---+ +---+ +---+
// clk -+ +---+ +---------+---------+ +---+
// +-----------------------
// a ------------------------+
// <--1us----><--1us--->
// Missing in requirements:
// 1. Clock period of the ref_clk and clk
// 2. Is clk derived from ref_clk?
// I'll also assume that one half period of clk is 125ns
//
module m;
bit clk, a;
initial forever #125 clk = !clk;
task automatic t_clk2a2clk(); // called by negedge clk
realtime then, v_clk, v_a;
then=$realtime;
fork
begin
@(posedge a) v_a= $realtime;
end
begin
@(posedge clk) v_clk=$realtime;
end
join_any
if (v_clk-then==125ns) disable t_clk2a2clk; // regular clk going
am_neg_clk2a: assert(v_a-then==1000ns); // first occurrence of a
@(posedge clk) am_a2neg_clk: assert($realtime-v_a==1000ns);
endtask
always @(negedge clk) fork t_clk2a2clk(); join_none;
initial #4000 $finish;
endmodule
Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.
// Using the ref clk
Untested, needs work, but the concept is there
bit clk, a, ref_clk;
initial forever #1 ref_clk = !ref_clk;
// assume 8 ref_clk equal one clk
// ref_clk 1 0 1 0 1 0 1 0 1 0 1
// clk 1 1 0 0 0 0 1 1 1 1 0
// | ^
// assume that clk is derived from ref_clk,
// thus posedge ref_clk causes a posedge or negedge of clk in the NBA of ref_clk
// e.g., always @(ref_clk) if(..) clk <= !clk;
let n=4; let m=4;
ap_1000ns: assert property(
@(negedge clk) ##0 @(posedge ref_clk) 1[*3] ##0 clk==0 |-> // start of dead cycles
##4 clk==0 && a==0 [*n] ##4 clk==0 && a==1 [*m] ##4 clk==1);
// n and m need to be calculated
```
https://www.edaplayground.com/x/UC_FHi Ben,
Thanks for the solution. I think this is suitable for my case. It gave me a lot of idea on how I should proceed. I implemented it as below to make it independent of ref clock.
My requirement is to make it at least 1us, not exactly 1us. Sorry for missing information.
I have ref clocks at 2 times higher frequency.
I was actually having issue for the check from clock stop time to A triggering time.
For the time check from A triggering until clock start, I used immediate assertion.
Here is my implementation.
// This part is for checking from clk stops until A is asserted.
always @(posedge clk or negedge clk)
clk_active_time = $realtime(); // always capture the last event time
property before_A_chk;
(($realtime - clk_active_time) >= 1us);
endproperty
assert_before_a_time: assert property (@(posedge A) before_A_chk);
Thanks
initial forever #1 clk = gate && !ref_clk;
/* I implemented it as below to make it independent of ref clock.
My requirement is to make it at least 1us, not exactly 1us.
I have ref clocks at 2 times higher frequency.
I was actually having issue for the check from clock stop time to A triggering time.
For the time check from A triggering until clock start, I used immediate assertion. */
// This part is for checking from clk stops until A is asserted.
realtime clk_active_time;
always @(posedge clk or negedge clk)
clk_active_time = $realtime(); // always capture the last event time
property before_A_chk;
(($realtime - clk_active_time) >= 1us);
endproperty
assert_before_a_time_BAD: assert property (@(posedge A) before_A_chk); // NOT GUARANTEED
// Question: What happens if there is no edges of clk except that
// (posedge clk or negedge clk) occurs in the
// exact time step as (posedge A) at time "t"
// +---+ +---+ +---+ +---+ +---+
// clk -+ +---+ +---------+ +----------+ +---+
// +-----------------------
// A -------------------------+(<-- time t)
// Answer: clk_active_time will be sampled in the Preponed Region at time t.
// The assertion is evaluated in the Observed Region.
// If clk_active_time is >= 1us in the Preponed region,
// then the assertion will PASS, but it should fail
// Conclusion: Good try!
//
// Using a reference clock:
let k=10; // minimum number of ref clk when clk==0
let max=100;
sequence s_dead_clk; // may be more simulation efficient
@(negedge clk) 1 ##0 @(posedge ref_clk) clk==0 [*k:max] ##0 @(posedge A) 1;
endsequence
ap_before_a_time: assert property (@(posedge A) s_dead_clk.triggered);
sequence s_dead_clk1;
//@(negedge clk) 1 ##0 @(posedge ref_clk) clk==0 [*k:max] ##0 @(posedge A) 1;
@(posedge ref_clk) clk==0 [*k:max] ##0 $rose(A) ; // OK too
endsequence
ap_before_a_time1: assert property (@(posedge ref_clk) s_dead_clk1.triggered);
I believe that my task solution covers all the cases.
Test it. You may also use the ref_clk solutions.
would something like this work? The before and after quiet period checks are in two separate assertions, easier to debug.
//minSeparation is the number of ref_clk tick that satisfy
// the minimum quiet period
A_before: assert property(@(posedge ref_clk)
not($fell(clk) ##[0:minSeparation] $rose(A)));
A_after: assert property(@(posedge ref_clk)
not($rose(A) ##[0:minSeparation] $rose(clk)));
Cannot run it to check correctness…
I missed a key element in my previous reply, sorry!
Let’s go back to the requirements:
// +---+ +---+ +---+ +---+ +---+
// clk -+ +---+ +---------+ +----------+ +---+
// +-----------------------
// A -------------------------+(<-- time t)
let k=10; // minimum number of ref clk when clk==0
let max=100;
ap_clk_0_to_A: assert property(@(posedge ref_clk) $fell(clk) ##1 !clk |-> //!clk[*2] |->
##1 clk==0 && A==0[*k:max] ##1 $rose(A) && clk==0) ;
ap_A_1_4K_clk_0: assert property(@(posedge ref_clk) $rose(A)|->
##1 clk==0 && A==1[*k:max] ##1 $rose(clk)) ;
Hi Ben,
I’ll try your solutions soon with the actual design and let you know.
Thanks for your catch. I gave it a thought. Why do you think it is expected to fail when (posedge A) and (posedge clk or negedge clk) occur at the same time. I expect it to pass since it is stable until (posedge A). It is actually okay for me to catch this kind of errors before or after (posedge A). But what I expect is that it should fail for not being stable for at least 1us after (posedge A).
Here is my implementation for checking at least 1us time condition after (posedge A). It will fail since there is a negedge happening just after (posedge A).
always begin
@(posedge A);
A_posedge_time = $realtime;
@(posedge clk or negedge clk);
posA_to_clk_active = $realtime - A_posedge_time;
assert_after_condition: assert (posA_to_clk_active >= 1us) begin
`uvm_info(...)
end else begin
`uvm_error(...)
end
end
What are your thoughts on this?
I just want to extend the discussion a bit further. Assume that there are many CLKs which should satisfy before and after 1us condition. refclk is always faster but not necessarily the input for A signal and CLK generation. Will your solution work for that case?
I can use your solution in many scenarios. It is simpler than mine. I am glad for giving such an elegant solution.
The good side of my solution is that it is independent of refclk.
[YOU] I’ll try your solutions soon with the actual design and let you know.
Thanks for your catch. I gave it a thought. Why do you think it is expected to fail
when (posedge A) and (posedge clk or negedge clk) occur at the same time.
I expect it to pass since it is stable until (posedge A).
It is actually okay for me to catch that error before or after (posedge A).
But what I expect is that it should fail for not being stable for at least 1us after (posedge A).
[Ben] Your original drawing for the requirements had clk==0 @(posedge A).
Let me change my solution to take care of the clk in the consequent
let k=10; // minimum number of ref clk when clk==0
let max=100;
ap_clk_0_to_A: assert property(@(posedge ref_clk) $fell(clk) ##1 !clk |-> //!clk[*2] |->
##1 clk==0 && A==0[*k:max] ##1 $rose(A)) ;
// Thus, after the detection of the start of no CLK |->
// I expect A==0 until a rose(A)
// New
ap_clk_0_at_A: assert property(@(posedge ref_clk) $rose(A) |-> clk==0);
//
//Ed gave you this solution that looks OK but it looks computational intensive
// Also, imho the "not" is hard to follow.
A_before: assert property(@(posedge ref_clk)
not($fell(clk) ##[0:minSeparation] $rose(A)));
A_after: assert property(@(posedge ref_clk)
not($rose(A) ##[0:minSeparation] $rose(clk)));
// Cannot run it to check correctness…
[You] Here is my implementation for checking at least 1us time condition after (posedge A).
It will fail since there is a negedge happening just after (posedge A).
always begin
@(posedge A);
A_posedge_time = $realtime;
@(posedge clk or negedge clk); // <<<<<
posA_to_clk_active = $realtime - A_posedge_time;
assert_after_condition: assert (posA_to_clk_active >= 1us) begin
`uvm_info(...)
end else begin
`uvm_error(...)
end
end // What are your thoughts on this?
// [Ben] WHy the negedge here? clk==0 during quiet time.
// Could it be quiet at clk==1?
// Can you have a posedge A while the clk is running and not on standby? that will ketch it
// you could rewrite this using a concurrent assertion
property p;
realtime A_posedge_time;
@ (posedge A) (1, A_posedge_time = $realtime) ##0 @(posedge clk) ($realtime - A_posedge_time) >= 1us;
endproperty
ap: assert property(p);
// I am generally very skeptical/cautious when using the "always begin @(ev) ..."
// because that process locks and will miss another 'ev' if the process was not terminated.
// In concurrent assertions you start a new thread with each attempt.
[You] Assume that there are many CLKs which should satisfy before and after 1us condition. refclk is always faster but not necessarily the input for A signal and CLK generation. Will your solution work for that case? I can use your solution in many scenarios. It is simpler than mine. I am glad for giving such an elegant solution.
[Ben] I gave you some solutions using automatic tasks triggered by an initialted condition.
You can try tht for simulation, but not for formal.
I noticed that when I am presented with a challenging assertion, I rephrase the problem in terms of automatic tasks. This, btw, is my description of the SVA model in my paper.
In some case, I can convert that task model into SVA.
What also helps is rephrasing the requirements and even ask AI (perplexity.ai) to rewrite them in bullet points (which can then be converted to SVA).