A constant SVA cycle delay within a range?

SystemVerilog
, ,
1

I’m trying to write formal-friendly SVA properties for the following requirement.

$rose( req ) |-> ##N ack;
Where N is a fixed deterministic delay that is a function of the design implementation. Any value for N from 1 to 10 is acceptable, as long as the delay does not change from one req->ack to the next.

I could first run a sim to measure the delay and then insert that value, but I prefer to keep my property more true to the requirement.

I could write a non-SVA counter that measures the delay and stores the result in a variable. I could then assert that the measured value is $stable(). Basically replicating my first idea, but in code. Anything better?

2

In reply to warnerrs:
You could do something like to measure the needed delay.


/* If the variable used to define the delay has values that are within a constraint range, such as between 0 and 7 (or 15, or at most 32) one can use the generate statement, which appears much simpler than the use of local variables and the sequence_match_item. Example: */
let v=10;
let max= 10;
let s=0;
generate for (genvar g_i=s; g_i<max; g_i++) begin
  ap_delay_gen: assert property (v==g_i && $rose(a) |-> ##g_i b);
end endgenerate

Then when you find out which value works for you, set the values of the lets. For example, assume that the assertion that works OK is with a dely of 5. You can then change the lets to:


let v=5; // your desired delay
let max= 6;
let s=5;
// The generate statement is NOT changed. 
generate for (genvar g_i=s; g_i<max; g_i++) begin
  ap_delay_gen: assert property (v==g_i && $rose(a) |-> ##g_i b);
end endgenerate

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr

3

In reply to ben@SystemVerilog.us:

Ben, Thanks for you ideas. That example still requires that I determine what the actual delay is, and then modify my checker. Your generate loop approach, however, did give me a couple of other ideas.

Here’s a solution that I really like for it’s conciseness and readability. I collect coverage on all of the delays, use a coverage action to get that information into a variable where I can test it, and then assert that the coverage is one hot.

Some simulators require that you enable coverage options to make the cover property’s pass statement work, so that’s a real negative here. I also doubt if formal tools can consume this code. My debug tools also do a poor job of tracing drivers for the cycle_delay[n] bits.

module same_cycle_delta2( input logic clk, enable,
                          input logic a, b );

	default clocking cb@( posedge clk); endclocking

	A_no_overlaps: assume property( disable iff (!enable) a |-> b or !b ##1 ( !a throughout b[->1] ) );

	logic [10:0] cycle_delay;
	
	C_disable: cover property( !enable ) cycle_delay <= 0; // clear when disabled, like an RTL reset
	for( genvar N=0; N<=10; N++ ) begin: delay
		C_delay: cover property( disable iff (!enable) a ##0 !b[*N] ##1 b ) cycle_delay[N] <= 1'b1; 
	end	
	A_same_delta: assert property( disable iff (!enable) $onehot0( cycle_delay ) );
		
endmodule // same_cycle_delta2

Which finally lead me to this next solution. It doesn’t require any coverage options for it to work and my debuggers have no issues tracing driers through this code. Not sure about formal and $past in this context, but that’d be easy to replace with a shift register.

module same_cycle_delta3( input logic clk, enable,
                          input logic a, b );

	default clocking cb@( posedge clk); endclocking

	A_no_overlaps: assume property( disable iff (!enable) a |-> b or !b ##1 ( !a throughout b[->1] ) );

	logic [4:0] cycle_delay, n_cycle_delay;

	always @(posedge clk or negedge enable) begin
		if (!enable)
		  cycle_delay <= 0;
		else
		  cycle_delay <= n_cycle_delay;
	end

	// How can this be generated concisely in a generate loop?
	assign n_cycle_delay[0] = cycle_delay[0] || a && b;
	assign n_cycle_delay[1] = cycle_delay[1] || $past(a,1) && !a && b ;
	assign n_cycle_delay[2] = cycle_delay[2] || $past(a,2) && !$past(a,1) && !a && b ;
	assign n_cycle_delay[3] = cycle_delay[3] || $past(a,3) && !$past(a,2) && !$past(a,1) && !a && b ;
	assign n_cycle_delay[4] = cycle_delay[4] || $past(a,4) && !$past(a,3) && !$past(a,2) && !$past(a,1) && !a && b ;
	
	A_same_delta: assert property( disable iff (!enable)
											 $onehot0( cycle_delay ) );
		
endmodule

I made a few attempts at creating a generate loop for the n_cycle_delay logic, however it kept getting messy and unreadable.

I was thinking I should also try an approach using an ‘expect’ statement, but I expect I’ll bump into limited tool support for that.

-Ryan

4

In reply to warnerrs:
What bothers me about your post is that you seem to derive the requirements (e.g. #cycle delay) off the design; that should really come off the requirements.

On the $past in the assign statement, you need a clock.

Go from requirements to design verification, and not from design to requirements. Maybe I am missing something here.
Ben Ben@systemverilog.us

5

In reply to warnerrs:
What bothers me about your post is that you seem to derive the requirements (e.g. #cycle delay) off the design; that should really come off the requirements.

Thank you for feeling my pain. That said, it’s not really as bad as that.

The functional requirement is that the delay is between 0 and 10 cycles. The designer is free to pick any fixed delay within that range.

If that delay is a function of a FSM waiting to pull data from a shared resource, there is the potential for the delay to vary if there is contention and the FSM doesn’t have highest priority. It is the responsibility of the FSM to hide any variability in latency of accessing the shared resource.

The designer could tell me what latency he picked, and I could code that expected delay into the checker. But, that’s still only an expectation, rather than a requirement, and not much different than inspecting the RTL to figure it out myself. Also, any number of things could cause them to have to rejigger things, ultimately leading to a slightly different delay. I want my checker, not to care about changes like that, as long as they’re within the required range.

6

In reply to warnerrs:

I did find a good generate loop for that code. After I converted $past(a,#) to a shift register, the solution became apparent.


	assign     n_observed_delay[0] = observed_delay[0] ||   past_a[0] && /*!past_a[-1]*/  && b;
	for( genvar N=1; N<=10; N++ ) begin: delay
	    assign n_observed_delay[N] = observed_delay[N] || ( past_a[N] &&   !past_a[N-1:0] && b );
	end
7

In reply to warnerrs:
Have you considered doing something like the following using the intersect?
That constrains the b[->1] to a fixed time period.


let v=5; // your desired delay
let max= 6;
let s=5;
// The generate statement is NOT changed. 
generate for (genvar g_i=s; g_i<max; g_i++) begin
  ap_delay_gen: assert property (v==g_i && $rose(a) |-> 
                  b or 
                  (!b ##1 (!a throughout b[->1] intersect 1'b1[*g]));
end endgenerate

Anyway, something for you to think about.
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr