Verification Guild

A Community of Verification Professionals

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.

Modules

· Home
· Downloads
· FAQ
· Feedback
· Recommend Us
· Web Links
· Your Account

Advertising

Who's Online

There are currently, 39 guest(s) and 0 member(s) that are online.

You are Anonymous user. You can register for free by clicking here

Verification Guild: Forums

Forum FAQ

Usergroups

Profile

Digest

PSL Problem
Goto page 1, 2 Next

This forum is locked: you cannot post, reply to, or edit topics.

This topic is locked: you cannot edit posts or make replies.

Verification Guild Forum Index -> Assertions

View previous topic :: View next topic

Author

Message

romi
Senior
Senior

Joined: Feb 28, 2004
Posts: 88
Location: Minnesota

Posted: Wed Sep 08, 2004 1:16 pm Post subject: PSL Problem

I need a property for the following SBE logic. If there is a single bit error on an address I want to verify that the same address eventually gets written to scub out the error. So, more generally... If signalA and address==N then eventually signalB and address==N. Seems like I'd need an assert for every address. This could be in the millions. Any ideas? Thanks.

vhdlcohen
Industry Expert

Joined: Jan 05, 2004
Posts: 1237
Location: Los Angeles, CA

Posted: Wed Sep 08, 2004 2:40 pm Post subject:

Quote:

If there is a single bit error on an address I want to verify that
the same address eventually gets written to scub out the error.

So, more generally...

If signalA and address==N then eventually signalB and address==N.
Seems like I'd need an assert for every address. This could be in the millions.

I'll provide 2 solutions, one for SystemVerilog Assertions and one for PSL, since I think this audience is interested in both languages.

Code:

// SystemVerilog Assertions
// Assuming a default clock
// More than one error can be handled (no limit here since
// local variable is local to the property
property pAddrErrorRewrite;
int vaddr; // local variable for addr
(write && addr_error, vaddr=addr) |=> // if error, store address in variable
##[0:$] write && !addr_error && addr==vaddr;
assert property (pAddrErrorRewrite);

Code:

// PSL, Verilog flavor, assuming a default clock
// Only one error allowed. If more than one error, the property
//will not check the other errors. The increment and reset of "error_count" is not
// shown here, but is handled by HDL code.
int vaddr;
always @ (posedge clk)
if (addr_error && error_count==0) vaddr <= addr;

property pAddrErrorRewrite =
always {write && addr_error && error_count==0}
|=> [*]; {write !addr_error && addr==vaddr};
assert pAddrErrorRewrite ;

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

romi
Senior
Senior

Joined: Feb 28, 2004
Posts: 88
Location: Minnesota

Posted: Wed Sep 08, 2004 2:56 pm Post subject:

Code:

Is the above extra verilog code needed to capture the address at the time of the SBE for the PSL example ?

Would you say your 2 examples show that system verilog has an advantage in that it can store information whereas PSL needs the "extra" verilog to do it?

In my opinion the PSL example is not usable because I want to make sure all SBEs get scrubbed not just the first one.

vhdlcohen
Industry Expert

Joined: Jan 05, 2004
Posts: 1237
Location: Los Angeles, CA

Posted: Wed Sep 08, 2004 3:21 pm Post subject:

Quote:

Is the above extra verilog code needed to capture the address at the time of the SBE for the PSL example ?

YES

Quote:

Would you say your 2 examples show that system verilog has an advantage in that it can store information whereas PSL needs the "extra" verilog to do it?

You go it! Unfortunately, PSL did not yet implement local variables in properties. Having local variables in threads is important for many classes of properties. Even though I am on the PSL committee, I am only one vote!

Quote:

In my opinion the PSL example is not usable because I want to make sure all SBEs get scrubbed not just the first one.

My PSL model limited itself to one error for simplicity. With some creativity in the HDL, you can implement more than one error. One thing that comes to mind is an array of depth "n" that stores the bad addresses. You can then use a function "exists" that returns TRUE if that address in one of those in error. The property would then look like this:

Code:

property pAddrErrorRewrite =
always {write && addr_error }
|=> [*]; {write !addr_error && exists(addr) &&
addr==vaddr};
assert pAddrErrorRewrite ;

For those interested in this methodology, SystemVerilog LRM 4.9 addresses Associative arrays, and methods that support them, including the "exists" function. In my FAQ book I demonstrated the use of an associative array in VHDL built with a VHDL linked list.
Ben

Note from the Editor: this topic was split into this thread
_________________
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

alexg
Senior
Senior

Joined: Jan 07, 2004
Posts: 586
Location: Ottawa

Posted: Wed Sep 08, 2004 5:19 pm Post subject:

In my opinion, Verilog is still a good choise for such checks in dynamic simulation.

Assuming that N is maximum amount of errors happening one after another (in real life, this number is always limited), and M is address width, 5 lines of Verilog code implement this check:

Code:

vc_stack #(N,M) addr_stack ();
always @(posedge clk) begin
if (write && error) addr_stack.add(address);
if (write && !error) addr_stack.check(address);
end

Here, vc_stack is verification component used to store & match addess values. Built-in "add" task adds address to stack, and "check" task removes the matching one. At the end of simulation, each instantiation of vc_stack will self-check whether it's pointer equals to 0 and produce an error otherwise.

Regards,
Alexander Gnusin

romi
Senior
Senior

Joined: Feb 28, 2004
Posts: 88
Location: Minnesota

Posted: Wed Sep 08, 2004 6:44 pm Post subject:

Quote:

In my opinion, Verilog is still a good choise for such checks in dynamic simulation.

Is doing multiple forms of dynamic verification to get similar errors seem like a hassle to you? For instance, if there are verilog checks like the one you suggested in someone's code along with PSL checks, isn't the process of detecting and debugging the errors somewhat different for each type? It seems like SVA is a more all encompassing solution.

Maybe this isn't a big problem, just wondering... Thanks.

cindy
Industry Expert

Joined: Aug 17, 2004
Posts: 309

Posted: Thu Sep 09, 2004 1:20 am Post subject:

romi, ben, alex, extra verilog code is NOT needed to express this property in psl! it can be done as follows: assert forall vaddr[0:31] in boolean: {write && addr_error && addr[0:31]==vaddr[0:31]} \|=> { [*]; write && !addr_error && addr[0:31]==vaddr[0:31]}; as you can see, the forall construct is playing the role of sampling the value of addr here. cindy.

Ajeetha
Senior
Senior

Joined: Mar 29, 2004
Posts: 424
Location: Bengaluru, India

Posted: Thu Sep 09, 2004 1:44 am Post subject:

cindy wrote:

assert
forall vaddr[0:31] in boolean:
{write && addr_error && addr[0:31]==vaddr[0:31]} |=>
{ [*]; write && !addr_error && addr[0:31]==vaddr[0:31]};

From LRM:

Quote:

If the parameter is an array of size N, then the property is replicated once for each possible combination
of N (not necessarily distinct) values from the set of values, with those values substituted for
the N elements of the array parameter. If the set of values has size K, then the total number of replications
is equal to K^N.

So won't this create 2^32 instances of this parameterized property with vaddrr substituted with values? If so, the Original poster was afraid of this at the first place - probably only few will be triggered in a simulation run.

I don't intend to favor one language or the other, but IMHO having dynamic variables is more optimal way to code such a property. But I agree, PSL has this capability - but in a rather limited way. Also with dynamic variables one could assign, check, re-assign within a long... sequence (SERE), again a real PSL expert may come up with a possible solution, but the point I am trying to make is the ease-of-use that Dynamic variables bring in.

Just my 2 cents worth..
Ajeetha
_________________
Ajeetha Kumari,
CVC Pvt Ltd. http://www.cvcblr.com
* A Pragmatic Approach to VMM Adoption http://www.systemverilog.us/
* SystemVerilog Assertions Handbook
* Using PSL/Sugar

cindy
Industry Expert

Joined: Aug 17, 2004
Posts: 309

Posted: Thu Sep 09, 2004 1:57 am Post subject:

Quote:

So won't this create 2^32 instances of this parameterized property with vaddrr substituted with values?

no!

The LRM text that you quoted is describing the functionality of the "forall" construct, not the implementation. A tool is free to implement the construct any way it wants, as long as the result is of the same functionality as that described in the LRM. IBM's tools do not implement "forall" by replication, and I would assume that the same holds for other vendors' tools as well.

I do see that the LRM text is easily misunderstood. I will file an errata request that it be reworded to emphasize functionality vs. implementation.

chrisw
Junior
Junior

Joined: Jan 07, 2004
Posts: 5

Posted: Fri Sep 10, 2004 12:46 pm Post subject:

Quote:

The LRM text that you quoted is describing the functionality of the "forall" construct, not the implementation. A tool is free to implement the construct any way it wants, as long as the result is of the same functionality as that described in the LRM. IBM's tools do not implement "forall" by replication, and I would assume that the same holds for other vendors' tools as well.

Cindy,

Do the IBM tools you mention include simulators?
I can see that for model checkers, replication is not needed. However, it is not clear that this is the case in a simulation environment. I can see three ways that a simulator may compile an assertion with a quantified variable.

1. replication of the property by explicit enumeration of the quantified variable.
2. replication by implicit (symbolic) enumeration of the quantified variable.
3. transform the property to operate on a time history of the quantified variable
such that only values that appear during simulation are enumerated (this is
similar to parameterization in symbolic simulation.)

The number of property evaluations for method 1 is O(T2^N) where T is the number of simulation time steps and N is the size of the quantified variable. For method 2, the number of evaluations per time step is N instead of 2^N, however, if the simulator uses BDDs to represent the variable and the value is randomly generated, which is likely to be the case for an address as in the example, then the overall complexity remains the same as case 1. For case 3, the number of evaluations per time step is T since only values seen during simulation need be considered and the total number of property evaluations is O(T^2).

For the example given, N=32, and with T=1,000,000 for example, method 3 clearly wins. However, if N=16 and T=1,000,000, method 1 or 2 wins. However, in either case, a huge number of evaluations are being done during a simulation run, which could have a drastic effect on simulation performance. Since it is not generally known at compile time how many time steps are going to be simulated, there is no way for the compiler to know which is the best method to use to compile the assertion. I can easily see simulator vendors thinking the safest choice is to simply to explicitly replicate and then put the burden on the user to fix any resulting performance problem.

On the other hand, an auxilliary array that stores addresses that had errors on them would allow reducing the number of property evaluations to O(T lgT) since only addresses with errors would require evaluation and it takes at most O(lgT) time to search the auxilliary array for an address. So, unless I am missing something, it seems that while it is possible to code properties without using auxilary variables, there may be a performance advantage in using them.

Regards,

Chris Wilson

cindy
Industry Expert

Joined: Aug 17, 2004
Posts: 309

Posted: Sun Sep 12, 2004 4:12 am Post subject:

chris,

Quote:

Do the IBM tools you mention include simulators?

yes. actually, what we have is a tool that translates psl into hdl checkers, which can then be used with any simulation tool.

Quote:

I can easily see simulator vendors thinking the safest choice is to simply to explicitly replicate and then put the burden on the user to fix any resulting performance problem.

that would be a very dumb thing for a simulation vendor to do.

Quote:

So, unless I am missing something, it seems that while it is possible to code properties without using auxilary variables, there may be a performance advantage in using them.

you are indeed missing something. you are getting hung up on the differences between quantified and dynamic variables, without recognizing that in a very large subset of the cases, one can be translated into the other and vice versa. for this large subset, there is obviously no difference in the efficiency with which they can be implemented.

cindy.

chrisw
Junior
Junior

Joined: Jan 07, 2004
Posts: 5

Posted: Sun Sep 12, 2004 4:44 pm Post subject:

Quote:

OK, then, can you explain how the your SBE assertion is translated using your tool? Is it done by introducing dynamic variables? What is the asymptotic simulation complexity?

In general, are all properties with forall constructs translated by introducing dynamic variables? Under what circumstances is it not possible to translate a forall to a dynamic variable?

thanks,

--chris

cindy
Industry Expert

Joined: Aug 17, 2004
Posts: 309

Posted: Wed Sep 15, 2004 3:47 am Post subject:

Quote:

OK, then, can you explain how the your SBE assertion is translated using your tool? Is it done by introducing dynamic variables?

sorry, but i am not at liberty to give details of our implementation. in general, i can say that it involves creating checkers on an as needed basis. i also need to note that we have a patent pending on the method.

Quote:

What is the asymptotic simulation complexity?

worst case is T^2 (assuming the size of the checker itself is negligible). i don't think you can do better with explicit dynamic variables: just because a property has single dynamic variable in it does not mean that you can use a single dynamic variable to evaluate the property. for instance, in our example, suppose that there are multiple write errors outstanding. then somehow you need to keep track of all of them.

i think (perhaps i'm wrong) that many people are confused by this: the term "dynamic variable" leads you to think that it is a variable like any other you would declare and use in a piece of code, when in reality it is a much more complicated thing.

Quote:

In general, are all properties with forall constructs translated by introducing dynamic variables? Under what circumstances is it not possible to translate a forall to a dynamic variable?

i don't know the answer off the top of my head, and i am traveling at the moment so don't have access to my colleagues. i'll check with them and get back to you on this one.

vhdlcohen
Industry Expert

Joined: Jan 05, 2004
Posts: 1237
Location: Los Angeles, CA

Posted: Wed Sep 15, 2004 2:57 pm Post subject:

Reconsidering the example:

Code:

assert
forall vaddr[0:31] in boolean:
{write && addr_error && addr[0:31]==vaddr[0:31]} |=>
{ [*]; write && !addr_error && addr[0:31]==vaddr[0:31]};

property pAddrErrorRewrite;
int vaddr; // local variable for addr
(write && addr_error, vaddr=addr) |=> // if error, store address in variable
##[0:$] write && !addr_error && addr==vaddr;
assert property (pAddrErrorRewrite);

It looks to me that from an implementation standpoint, the real difference between a SystemVerilog assertion variable and a PSL "forall" is the following:
- SystemVerilog uses an explicit user defined assertion variable
- PSL uses an implicit, non-user defined, variable available to the simulation tool.
Using the above example, in both languages, if the antecedent is TRUE, the variable for the address and other information, such as the thread ID, get stored into a hash table.
When the consequent for that thread gets checked, the contents of that hash table is used in the comparison. This may be optimized such that if all the preconditions are TRUE (e.g., write && !addr_error ), then the table is accessed.

Thus, the size of the forall argument is irrelevant, and as Cindy mentioned, replication is not needed.

Having said all of that, it would seem to me that adding assertion variables to PSL would not be a big impact for EDA vendors.
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

cindy
Industry Expert

Joined: Aug 17, 2004
Posts: 309

Posted: Thu Sep 16, 2004 4:01 am Post subject:

Quote:

Having said all of that, it would seem to me that adding assertion variables to PSL would not be a big impact for EDA vendors.

adding assertion variables to psl would be a big impact to the language, from a conceptual point of view.

our main goal in designing psl was simplicity and clarity: not only did we want to give it formal semantics, we wanted to give it formal semantics that were easily and intuitively understood by the typical user.

the precise meaning of a "forall" statement is trivial to explain: it is equivalent to replicating the formula, although it may be implemented in a much more efficient manner.

the precise meaning of a dynamic variable is not so easy to explain. to those who are used to programming and/or hardware description languages, it seems intuitive and therefore deceptively simple. but there are so many delicate corner cases: what happens if you "or" two sequences together and both of them contain an assignment to the same dynamic variable: is the value of that variable at the end of the or'ed sequence the value assigned in the left hand side of the "or" or the value assigned in the right hand side? if the left hand side is matched, it should be the value assigned in the left hand side. if the right hand side is matched, it should be the value assigned in the right hand side. but what if both sides are matched?

and what happens if you "or" two sequences together and only one of them contains an assignment to some dynamic variable: what then is the value of that variable at the end of the or'ed sequence? again, if only one side is matched, then the answer is easy: either the value assigned by the side that assigns a value, if it happens to match, or undefined, if the other side matches. but again, what if both sides match?

and what if there is a starred sub-sequence so that a single, non-or'ed sequence can match at multiple times? for instance, consider

Code:

always ({ a ; b[*] ; c } |=> { d ; e ; f })

suppose that you wanted to assign a dynamic variable at the point where "c" is asserted in the left hand side of this implication, and use it somewhere on the right. well, if you have a trace such that "a" is asserted in cycle x, b is asserted in cycles x+1 and x+2, and c is asserted in cycles x+2 and x+3, what is the sampled value of the dynamic variable? the answer, of course, is that since both "matches" of the left hand sequence {a;b[*];c} must be considered, there are really two instances of the single dynamic variable, one sampled at time x+2 and used for the shorter "match" of the left hand side, and one sampled at time x+3 and used for the longer "match".

it is possible to define all of this formally, but the result is extremely complicated, to the point where even an expert needs to sit down and really concentrate to make sense of a corner case; the apparent simplicity of dynamic variables in an assertion language is just an illusion. as i said, our main objective in psl was clarity, and therefore we chose to provide the capabilities of dynamic variables through the much simpler, easy to define and easy to explain mechanism of "forall".

Display posts from previous:

	Verification Guild Forum Index -> Assertions	All times are GMT - 5 Hours Goto page 1, 2 Next
Page 1 of 2

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

Forums ©

Verification Guild © 2006 Janick Bergeron
Web site engine's code is Copyright © 2003 by PHP-Nuke. All Rights Reserved. PHP-Nuke is Free Software released under the GNU/GPL license.
Page Generation: 0.368 Seconds