| Login | | Don't have an account yet? You can create one. As a registered user you have some advantages like theme manager, comments configuration and post comments with your name. | |
| Who's Online | There are currently, 51 guest(s) and 0 member(s) that are online.
You are Anonymous user. You can register for free by clicking here | |
 | |
|
Verification Guild: Forums |
|
| View previous topic :: View next topic |
| Author |
Message |
romi
Senior
Joined: Feb 28, 2004
Posts: 88
Location: Minnesota
|
 Posted: Mon Nov 08, 2004 3:57 pm Post subject: Timeout assertion |
 |
|
One of the most common and useful type of assertion we use in our design is what I'll call a "timeout" assertion. Typically, it can be reduced to if ‘a’ happens then within approximately ‘x’ number of cycles ‘b’ should occur.
Because of the many modes we run in, it’s almost always necessary to have ‘x’, the number of cycles before a timeout, be programmable. Because ‘x’ is typically just a best guess, the timeout value does not have to be exact. So, we use a single common timer along with assertion specific logic which programmatically taps off a bit of the timer (N) and looks for 2 toggles of the particular bit that is selected. This makes it so only 1 bit is needed to time a particular piece of logic and not a complete timer. Although the accuracy is only within 2^(N) to 2^(N+1), it’s close enough for us.
Currently, all of our assertions are coded in Verilog. I was hoping writing PSL could simplify the assertion and eliminate the extra verilog logic that is needed for the timer, but I can’t figure out a way to change the assertion timer value at run time. For instance, in this (illegal) PSL assertion:
| Code: |
property active_timer =
forall i in [0:`W]:
always ( {active_s[i]} |=> {[*0:<TIMER>];!active_s[i]}!);
assert active timer;
|
I’d like to be able to set TIMER at run time. Any ideas on alternative ways of accomplishing this? Thanks.
For completeness, below is the Verilog code that is used instead.
| Code: |
// Timer and programmable selector.
always @(negedge clk) begin
timer_r[31:0] <= timer_s[31:0] + 32'b1;
timer_sel_r[4:0] <= timer_sel_r[4:0];
end
assign timer_s[31:0] = timer_r[31:0];
assign timer_sel_s[4:0] = timer_sel_r[4:0];
// Watch selected bit
assign timer_clk_x = timer_s[timer_sel_s[4:0]];
always @(negedge clk) begin
timer_clk_r <= timer_clk_x;
end
assign timer_clk_s = timer_clk_r;
// Signal when selected bit toggles.
assign timer_toggle_x = timer_clk_s ^ timer_clk_x;
// Enable a timer when active is set and there is a toggle. Then, keep enabled
// until the active signal goes away.
always @(negedge clk) begin
timer_enabled_r[`W:0] <= (active_s[`W:0] & timer_enabled_s[`W:0]) | // Clear and Hold
({`W+1{timer_toggle_x}} & active_s[`W:0]); // Set
end
assign timer_enabled_s[`W:0] = timer_enabled_r[`W:0];
// Signal a timeout when another toggle is seen.
assign timeout_x[`W:0] = timer_enabled_s[`W:0] & {`W+1{timer_toggle_x}};
|
|
|
| Back to top |
|
 |
vhdlcohen
Industry Expert
Joined: Jan 05, 2004
Posts: 1238
Location: Los Angeles, CA
|
| Posted: Mon Nov 08, 2004 7:51 pm Post subject: |
|
|
| Quote: |
‘a’ happens then within approximately ‘x’ number of cycles ‘b’ should occur. |
Let me first provide a SystemVerilog Assertions solution because SVA has local variables.
| Code: |
'define true 1'b1
int max_cycles; // set dynamically during simulation
// typically at initalization of run,
// and then reset dynamically to a new value (via a force, or thru an assignment
// when the sets of tests are done, and new tests are needed.
property pA_then_B_beforeTimeout;
int v_timeout; // local variable, maintained for EACH THREAD
@ (posedge clk) disable iff (!reset_n)
($rose(a), v_timeout=0) |=> // for every thread and a new 'a'
(!b && v_timeout <=max_cycles, v_timeout +=1) [*0:$] ##1 b;
// as long as !b is true and variable v_timeout is less than or equals to the max_cycles
// increment v_timeout.
// property passes when b occurs and v_timeout <=max_cycles
// property fails if "v_timeout ==max_cycles" and at next cycle
// b is false.
endproperty : pA_then_B_beforeTimeout;
// Note that this property is applicable for every thread started when $rose(a)
|
| Quote: |
I was hoping writing PSL could simplify the assertion and eliminate the extra verilog logic that is needed for the timer, but I can’t figure out a way to change the assertion timer value at run time. For instance, in this (illegal) PSL assertion:
| Code: |
property active_timer =
forall i in [0:`W]:
always ( {active_s[i]} |=> {[*0:<TIMER>];!active_s[i]}!);
assert active timer; |
|
In Verilog you can create a pulse or a level identifying a timeout (called timeout), and identifying a property that states the failed condition.
| Code: |
`define W 1000
property pFailue4_a_then_b =
always (({rose(a)} |=> [*0:`W] ; timeout) abort b);
|
The problem with that code is that timeout timer must be started from "a", and
is really valid for one thread. It is not like the SVA solution where the variable is local to the property.
The other alternative is use a globally static constont (i.e., parameter) for TIMER, but then that does not meet your requirement to have that value dynamic at run time. You'll have to recompile for each value of TIMER in the range.
Maybe not what you want to hear, but in PSL, as well as in SVA the range must be static. However, in SVA, one can use a local variable to create this equivalent dynamic range. I don't know of any way to do the same in PSL.
Ben
_________________
Ben Cohen http://www.systemverilog.us/
* SystemVerilog Assertions Handbook, 3rd Edition, 2013
* A Pragmatic Approach to VMM Adoption
* Using PSL/SUGAR ... 2nd Edition
* Real Chip Design and Verification
* Cmpt Design by Example
* VHDL books |
|
| Back to top |
|
|
|
|
You can post new topics in this forum
You can reply to topics in this forum
You cannot edit your posts in this forum
You cannot delete your posts in this forum
You cannot vote in polls in this forum
|
| |
|
|
Forum FAQ
Search
Usergroups
Profile
Digest
Log in
