| 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, 49 guest(s) and 1 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 |
cindy
Industry Expert
Joined: Aug 17, 2004
Posts: 309
|
 Posted: Mon Jan 03, 2005 3:15 am Post subject: |
 |
|
harry,
| Quote: | | Certainly having an unambiguous specification is desirable for IP and dersign reuse. However, there is also a danger in over specifying a design in the early stages--since it too quickly limits the designer's degrees of freedom necessary for exploring various implementations, which is important for optimization (in terms of speed, area, power, etc.). Ambiguity is not necessarily a bad thing... |
i respectfully disagree. while the concepts of ambiguity/clarity are certainly related to those of over/under-specification, the two don't necessarily go hand in hand. that is, you can can an ambiguous specification which is over-specified, and you can have an unambigous specification which leaves degrees of freedom.
for instance, consider a bus protocol. you can over-specify by stating that in such-and-such a case, the snoop response must be retry, when in actuality there might be a more efficient implementation that does not retry in such a case. the same specification may be ambiguous because it says in english "a non-retry snoop response is not allowed for 3 cycles after an unsuccessful snoop response", without specifying what is meant by the term "unsuccessful snoop response".
by the same token, you can be unambiguous by stating every requirement in a property specification language, but under-specify by not stating enough requirements. (to top it off, you can unambiguously under-specify by stating explicitly that "in such-and-such a case, any snoop response is legal. the details are left up to the implementation").
cindy. |
|
| Back to top |
|
 |
alexg
Senior
![]()
Joined: Jan 07, 2004
Posts: 586
Location: Ottawa
|
| Posted: Mon Jan 03, 2005 1:48 pm Post subject: |
|
|
| cindy wrote: |
no, this is not correct. to use |=> across clock domains in psl, simply clock the lh-sere and the rh-sere separately, like this:
| Code: | | {a;b;c}@clk1 |=> {d;e;f}@clk2 |
cindy. |
Could you please point me to the place in PSL Specification where this construct (SERE1@clk1 |=> SERE2@clk2) is defined. I can only find cross-clock domain Sequence => FL Property definition (6.2.1.6). Then, there are multiply-clock definitions of SEREs and FL properties, but without suffix implication operator "|=>".
In general, I think that PSL Specification lacks the "multiple clock support" section, such as section 17.12 of SystemVerilog specification.
-Alex |
|
| Back to top |
|
|
alexg
Senior
![]()
Joined: Jan 07, 2004
Posts: 586
Location: Ottawa
|
| Posted: Tue Jan 04, 2005 1:22 am Post subject: |
|
|
| harrydfoster wrote: | Certainly having an unambiguous specification is desirable for IP and dersign reuse. However, there is also a danger in over specifying a design in the early stages--since it too quickly limits the designer's degrees of freedom necessary for exploring various implementations, which is important for optimization (in terms of speed, area, power, etc.). Ambiguity is not necessarily a bad thing...
|
High-level verification may help to refine specification requirements. This obviously requires partial high-level modeling. Upon successful verification, both properties and high-level implementation details will co-exist in Specification document.
Generally speaking, I think that it is dangerous to separate specification and implementation. If it happens, it complicates as design, as verification process. Usually, specification documents contain as elements of specification, as elements of implementation. High-level implementation refines specification, and vice versa.
| "vhdlcohen wrote: |
At startup, the TAP is forced to the Test-Logic-Reset state by asserting TRST_f low (note that holding TMS high for five TCK cycles also reaches Test-Logic-Reset from any state).
Notice that the specification makes reference to a note , something that may not be needed or skipped, after all, it's a "note".
The following code clarifies the above statement:
Code:
In PSL, that could have been written as:
property StateAfterReset = always TRST_f -> tap.tap_fsm== 0;
property StateAfter5TMS =
always {rose(TMS); [*4]TMS} |=> {tap.tap_fsm== 0};
Note that the spec makes reference to an FSM and its internal critical states.
|
This is a good example of high-level implementation. TAP Controller FSM diagram is a part of Specification document too. The property of reseting FSM using 5 consequent high TMS cycles is built-in into this FSM. So, if we copy this FSM into our implementation, why to bother checking this property in RTL?
On the other hand, humans make errors everywhere and chip achitects are humans too  So, before appearing in Specification, Tap Controller FSM has to be verified against this property. Formal methods may be extremely useful here. The following code is a working example of such verification using NuSMV input language (http://nusmv.irst.itc.it/) with LTL specification:
| Code: |
MODULE main
VAR
tms: boolean;
state: {TL_RESET, RUNT_IDLE, SEL_DR_SCAN, SEL_IR_SCAN,
CAPT_DR, SHIFT_DR, EXIT1_DR, PAUSE_DR, EXIT2_DR, UPDATE_DR,
CAPT_IR, SHIFT_IR, EXIT1_IR, PAUSE_IR, EXIT2_IR, UPDATE_IR};
ASSIGN
init(state) := TL_RESET;
TRANS
case
state = TL_RESET & tms = 0 : next(state) = RUNT_IDLE;
state = RUNT_IDLE & tms = 1 : next(state) = SEL_DR_SCAN;
state = SEL_DR_SCAN & tms = 0 : next(state) = CAPT_DR;
state = SEL_DR_SCAN & tms = 1 : next(state) = SEL_IR_SCAN;
state = CAPT_DR & tms = 0 : next(state) = SHIFT_DR;
state = CAPT_DR & tms = 1 : next(state) = EXIT1_DR;
state = SHIFT_DR & tms = 1 : next(state) = EXIT1_DR;
state = EXIT1_DR & tms = 0 : next(state) = PAUSE_DR;
state = EXIT1_DR & tms = 1: next(state) = UPDATE_DR;
state = PAUSE_DR & tms = 1 : next(state) = EXIT2_DR;
state = EXIT2_DR & tms = 1 : next(state) = UPDATE_DR;
state = EXIT2_DR & tms = 0 : next(state) = CAPT_DR;
state = UPDATE_DR & tms = 0 : next(state) = RUNT_IDLE;
state = UPDATE_DR & tms = 1 : next(state) = SEL_DR_SCAN;
state = SEL_IR_SCAN & tms = 0 : next(state) = CAPT_IR;
state = SEL_IR_SCAN & tms = 1 : next(state) = TL_RESET;
state = CAPT_IR & tms = 0 : next(state) = SHIFT_IR;
state = CAPT_IR & tms = 1 : next(state) = EXIT1_IR;
state = SHIFT_IR & tms = 1 : next(state) = EXIT1_IR;
state = EXIT1_IR & tms = 0 : next(state) = PAUSE_IR;
state = EXIT1_IR & tms = 1: next(state) = UPDATE_IR;
state = PAUSE_IR & tms = 1 : next(state) = EXIT2_IR;
state = EXIT2_IR & tms = 1 : next(state) = UPDATE_IR;
state = EXIT2_IR & tms = 0 : next(state) = CAPT_IR;
state = UPDATE_IR & tms = 0 : next(state) = RUNT_IDLE;
state = UPDATE_IR & tms = 1 : next(state) = SEL_DR_SCAN;
1: next(state) = state;
esac
LTLSPEC
G(tms = 1 -> X (tms = 1 -> X(tms = 1 -> X( tms = 1 -> X(tms = 1 -> X state=TL_RESET)))))
|
Regards,
Alexander Gnusin |
|
| Back to top |
|
|
cindy
Industry Expert
Joined: Aug 17, 2004
Posts: 309
|
| Posted: Tue Jan 04, 2005 6:58 am Post subject: |
|
|
alex,
| Quote: | | Could you please point me to the place in PSL Specification where this construct (SERE1@clk1 |=> SERE2@clk2) is defined. |
see p. 68 of lrm v1.1. one of the options shown for an fl property is
| Quote: | | Sequence |=> FL_Property |
a sequence, according to p. 46, can be a clocked sere. and so can an fl property (because an fl property can be a sequence, see p. 56).
| Quote: | | In general, I think that PSL Specification lacks the "multiple clock support" section, such as section 17.12 of SystemVerilog specification. |
after writing my explanation above, which involves three different lrm locations in order to show you how to write sere1@clk1 |=> sere2@clk2, i definitely agree with you. i'll propose adding clarifying text in the lrm.
thanks,
cindy. |
|
| Back to top |
|
|
jmb
Senior
Joined: Jan 11, 2004
Posts: 34
Location: California/Silicon Valley
|
| Posted: Thu Jan 06, 2005 4:50 pm Post subject: |
|
|
| Quote: |
Janick, my point is that there is a need in a requirements document and a verification plan document to define the requirements and the plans in a manner that is more "exact", "consice", and "unambiguous" than a natural language.
|
This is not a problem that is unique to verification - general software design researchers have been after something like this for decades. And failed. There is a lot that those of us in verification could learn from their failure. Just for starters, we should learn that we are not going to find an easy solution to this problem. More specifically, we should learn from what the software community has known for years:
Specifications in declarative languages look great in simple examples but fall apart on complicated ones.
Corner cases in the definition often lead to significant complications to the declarative description (i.e., lots of extra clauses all over the place - think of conditioning everything on "reset" in an ABV"). As a result, specifications in declarative languages may be "unambiguious" but they are rarley "consice" (except for simple cases).
Complex declarative specifications are often extremely difficult to debug and understand and the resulting confusion is worse than a slightly ambiguous (but interpretable) natural language description. Think about how hard it would be to ensure that, say, a 500-line assertion hits exactly all of the intended cases. In contrast, I've seen procedural code that is tens of thousands of lines long and easy to understand.
PSL/ABVs are great for simple things. The reason they don't work well at the transaction level is that transaction-level data checkers are often very complex - sometimes thousands of lines of code.
We should use them where they help - generally on simple, low-level aspects of the design. But they are not the "holy grail" or "silver bullet" for verification. |
|
| Back to top |
|
|
cindy
Industry Expert
Joined: Aug 17, 2004
Posts: 309
|
| Posted: Sun Jan 09, 2005 9:01 am Post subject: |
|
|
jmb,
| Quote: | | Think about how hard it would be to ensure that, say, a 500-line assertion hits exactly all of the intended cases. |
we are definitely in agreement on this. more than a few lines of psl per property is not the way psl is intended to be used.
| Quote: | | We should use them where they help - generally on simple, low-level aspects of the design. |
but not on this. i've seen and written myself many assertions on high-level aspects of a design that have been used to good effect.
| Quote: | | But they are not the "holy grail" or "silver bullet" for verification. |
and back to agreement. abv is a tool. like any tool, it can be used well or used poorly. although i do think that as tools improve and as users gain experience with writing effective assertions, it will become more common to use them well.
cindy. |
|
| Back to top |
|
|
jmb
Senior
Joined: Jan 11, 2004
Posts: 34
Location: California/Silicon Valley
|
| Posted: Mon Jan 10, 2005 3:10 pm Post subject: |
|
|
| Quote: |
and back to agreement. abv is a tool. like any tool, it can be used well or used poorly. although i do think that as tools improve and as users gain experience with writing effective assertions, it will become more common to use them well.
|
I don't have a problem with people using declarative languages like ABVs or PSLs in the somewhat limted cases where they provide clarity. But many people are claiming that they are much, much more than "any tool". For instance, earlier in this threead Alex said:
| Quote: |
My original premise though was that a property specification language like SVA or PSL can be used in a requirements document to specify intent.
|
If we are going to use PSLs as a specification language then they have to be able to be a complete specification. Yet this forum is riddled with examples of things that are impossible, difficult, or confusing to do in an ABV or PSL. The last of those 3 is the worst - if it is confusing then it defeats the purpose of a specification.
Things like "temporal assertions" are just kludges to help make the declarative languages a little bit procedural. And we now see people clamoring to have more and more "procedural" features added to these declarative langauges. Does this really make sense?
For real verification problems all of these declarative approachs at some point punt back to using procedural code - typically C/C++ or a subset triggerred by an assertion. So now we have a mixed-language approach to the problem because of the inadequacies of the declarative languages. This stikes me as a big step backwards.
In contrast, procedural langauges can do it all and have many, many years of development and refinement behind them. Those touting declarative langauges need to show examples of real, compete testbenches (not 10 line examples) which are superior to the equivalent procedural code. The approach at my company has been to embrace and exploit the power of procedural langauges (Perl, in our case) and I am strongly convinced that it is vastly superior to any of the declarative approaches being proposed.
I'll summarize here so that folks replying to me will have an easy time quoting me for their attacks:
The current batch of declarative langauges are not powerful or complete enough to allow them to be used as requirements languages.
Further, they will never be powerful enough and remain simple and concise. Lots of time has already been spent on this problem in the general world of software development over the last 30 years or so. I see no reason to believe that the verification community will somehow be able to succeed where a much larger community has failed. (a little more on this is at www.greenl.com/Denotational.htm)
Procedural languages provide all of the power we need to solve any verification problem and the result is cleaner than a mixed-langauge approach.
There are some limited places where I think that ABVs are PSLs are useful. They are just not "enough" to base an entire verification methodology on. |
|
| Back to top |
|
|
|
|
You cannot post new topics in this forum
You cannot 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
