| 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, 68 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 |
alexg
Senior
![]()
Joined: Jan 07, 2004
Posts: 586
Location: Ottawa
|
 Posted: Sat Aug 28, 2004 7:28 pm Post subject: How to best identify corner cases |
 |
|
Editor's note: this topic was split from this topic
Hi Tim,
I still have some comments:
| Quote: | | In the absence of sufficient specification it may be necessary to extract properties form RTL. In fact for a full formal verification it may be necessary to reverse engineer a complete block into properties, the sum of which describe its functionality (which may be proved by a theorem prover or perhaps just by pencil and paper). If this is necessary then there is all the more need to approach the job intelligently. |
I would separate functional verification from the reverse engineering. Reverse engineering of RTL code with designer sitting in the next cubicle is , IMHO, waste of time. Unfortunately, in some cases assertion methodology is interpreted as reverse engineering on design code, which reduces efficiency of the whole verification process. These are some of the reasons to avoid reverse engineering in verification:
1. Verification makes sense when the model is functional abstraction of implementation. For example, there is low value to re-implement FSM in another language or another way in order to verify it: RTL code is clear enough and the goal we achieve is still verification between implementation drawing of FSM and RTL code. I would not call this verification "functional", since functions or "features" of state machine still remain unverified.
2. With reverse engineering, it is difficult & time consuming & impossible to extract important functional features. Take, for example, TAP controller FSM. It is operated by single signal called TMS. There is a feature of this FSM described in the Spec: TMS signal, being high during 5 continuous clock cycles, brings FSM to the reset state from anyone of other states. This is important feature that can be easily verified with formal methods during FSM design. Is it possible to extract this feature definition from RTL code for the verification? I think, no.
3. DUT boundary is the natural border between verification engineers and designers. Everybody has experience in his own domain and lacks experience while playing on another territory.
Any verification including formal makes sense if we verify functional properties vs. implementation code. Verification of trivial properies (such as write is always inversion of read, having "assign write = ~read" statement in RTL) is nothing more than duplication of implementation in another way. Once more, real functional features will still remain unverified having both of these implementations in place.
In order to avoid reverse engineering, verification process should be combined with impementation code development. That's what verification engineers are doing when they put "debug" messages to important places once developing verification components. I don't think designers will be interested to dig into verification code to figure out the right places for these debug messages. This will be low-efficient and time-consuming task for designers. The same stands for verification engineers vs RTL code.
| Quote: | | I like the idea of formally verifying a high-level model of a system, e.g. to ensure no deadlocks or livelocks exist in the system. Which tools would you recommend for this? What languages do they use? Are you also suggesting that a high-level model could be used to determine suitable places for block boundaries, and which properties these blocks need to satisfy for the correct functioning of the system? |
There are two basic types of pre-RTL modeling:
1. Transaction-level modeling. This is not clock-precise modeling, where the function of block is written in higher-level non-RTL language. Blocks communicate using transactions, which are defined as data structure+simulation time+location/direction identifier. Transaction level modeling is important as for proof-of-concept, as for architecture definition and rough performance estimation. For TLM, dynamic verification can be used only.
2. Clock-precise modeling of FSMs or protocols. Usually, specification defines not only the features of given protocol or arbiter, but also implementation state machine or clock-precide protocol definition. During this process, verification of resulting protocol /FSM definition versus the features is extremely important. Formal tool can provide chip architects absolute confidence that "implementation" parts of Spec such as for example FSM diagram are complete and correct relative to their features. Dynamic verification with this type of modeling is also possible, but less efficient, less complete and more time-consuming comparing to the formal verification. I also believe that amount of state variables (registers) will be not an issue in this case, avoiding formal tools state explosion problems.
Speaking about tools, any commercial formal tool can be used for this purpose. There are also free tools such as SMV or NuSMV which can be used for this purpose as well. However, specification language for these tools (CTL) is more difficult to use than PSL.
Regards,
Alexander Gnusin |
|
| Back to top |
|
 |
elavelle
Junior
Joined: Jun 15, 2004
Posts: 9
|
| Posted: Sun Aug 29, 2004 11:59 am Post subject: |
|
|
| alexg wrote: |
I would separate functional verification from the reverse engineering. Reverse engineering of RTL code with designer sitting in the next cubicle is , IMHO, waste of time. Unfortunately, in some cases assertion methodology is interpreted as reverse engineering on design code, which reduces efficiency of the whole verification process. These are some of the reasons to avoid reverse engineering in verification:
<snipped>
3. DUT boundary is the natural border between verification engineers and designers. Everybody has experience in his own domain and lacks experience while playing on another territory.
|
I agree in principle, but this can cause problems in practice. In order to know what the interesting corner cases are, the verification engineer has to have some understanding of the RTL. The Pentium FPU bug was an obvious example: if the verification engineer had known about the implementation, then the bug would presumably have been trivial to find.
You might argue that the designer should put in the assertions to cover these corner cases, since the designer is the person who knows about them, and I'd agree. But the reality is that most designers have no idea how to specify assertions. A second issue is that we would then have to rely on the designer alone to verify complex internal corner cases, which would probably guarantee failure.
Evan |
|
| Back to top |
|
|
confused
Senior
![]()
Joined: Jan 09, 2004
Posts: 185
|
| Posted: Mon Aug 30, 2004 7:45 pm Post subject: |
|
|
| elavelle wrote: | In order to know what the interesting corner cases are, the verification engineer has to have some understanding of the RTL. The Pentium FPU bug was an obvious example: if the verification engineer had known about the implementation, then the bug would presumably have been trivial to find.
|
After understanding the specification well enough, some knowledge of design internals can sometimes help the verification engineer. I do not understand why such knowledge is required.
I do not know much about the Pentium FPU bug. It is hard to imagine why it is easy to find if the verification engineer knew the design well. If this is true, the design engineer would already have found it.
I worked on some similar FPU designs. Basically, the spec is the IEEE standard plus some op codes and operand representations. A Berkeley PhD's whole dessertation is to list tons of interesting tests for the compliance of this standard. It did not discuss the theory behind these tests, and therefore the test suite may not be complete. I checked with the design engineers years after the project, and they never identified coverage holes in the test suite. If it is trivial, they must not have worked hard. In fact, they still stay in the same organization and have got promotions. Maybe they were just lucky?
Design engineers are typically required to approve verification plans. They are often more or less involved in developing verification plans. These should be true for the verification of the Pentium FPU. |
|
| Back to top |
|
|
alexg
Senior
![]()
Joined: Jan 07, 2004
Posts: 586
Location: Ottawa
|
| Posted: Mon Aug 30, 2004 10:24 pm Post subject: |
|
|
Hi Evan,
please see my comments below.
| Quote: | | In order to know what the interesting corner cases are, the verification engineer has to have some understanding of the RTL. |
In order to know functional corner cases, verification engineer don't have to know implementation - all of them can be extracted from specification. If they require assertions or white box functional coverage - verification engineer has to implement them. However, definitions for these assertions and functional coverage monitors are still derived from Spec, and not from implementation RTL. The only information designer has to provide is the hierarchical path to these points. For example, protocol specification defines usually not only behavior of the interface signals, but also FSMs, which have to control these signals. Then, verification engineer may want to dig int RTL code in order to correlate that FSM state with information provided by the protocol monitors. However, in this case verification engineer knows exactly what he/she wants without the need of any reverse engineering. In his book, Janick classifies this type of assertions as functional (implementation assertions being another type).
| Quote: | | The Pentium FPU bug was an obvious example: if the verification engineer had known about the implementation, then the bug would presumably have been trivial to find. |
In any case, after reverse engineering verification engineer cannot achieve the same level of design understanding as designer has. I can turn this statement in a different way: if designer will run some formal checks during design and will supply to verification engineer not only RTL code, but also assertions/white box coverage metrics to target corner cases in his specific implementation, then the bug would presumably have been trivial to find, if it will not disappear yet.
| Quote: | | You might argue that the designer should put in the assertions to cover these corner cases, since the designer is the person who knows about them, and I'd agree. |
I've argued already 
| Quote: | | But the reality is that most designers have no idea how to specify assertions. |
In my experience, designers learn assertions and formal specification languages faster than verification engineers. Then, I understood why: assertions and PSL are cycle-precise and low-level, and designers live in low-level cycle-precise world. Verification engineers, in their turn, are sharing ther time between cycle-precise (developing low-level drivers and monitors) and more abstract transaction-level or object-oriented code development.
| Quote: | | A second issue is that we would then have to rely on the designer alone to verify complex internal corner cases, which would probably guarantee failure. |
Formal verification is about finding complex internal corner cases. If designer will write property in formal language such as PSL before writing the code, he/she will find then all complex corner cases where this property fails and correct them during implementation stage. It would be also more covenient for verification engineers to learn about implementation from these properties. It would be also important for chip architect to review these properties in order to make sure that designer's intent is well aligned with his own.
Regards,
Alexander Gnusin |
|
| Back to top |
|
|
tblackmore
Senior
Joined: Jan 23, 2004
Posts: 43
Location: Bristol, England
|
| Posted: Tue Aug 31, 2004 4:09 am Post subject: |
|
|
| Quote: |
In any case, after reverse engineering verification engineer cannot achieve the same level of design understanding as designer has
|
| Quote: |
Then, I understood why: assertions and PSL are cycle-precise and low-level, and designers live in low-level cycle-precise world. Verification engineers, in their turn, are sharing ther time between cycle-precise (developing low-level drivers and monitors) and more abstract transaction-level or object-oriented code development
|
Could I first say that reverse engineering code is not my preferred method of verification. But it can be necessary because (i) a block is inadequately specified and/or (ii) currently available formal verification tools are not good enough at reachable state analysis to make black-box formal verification of most blocks possible.
However when it is necessary to reverse engineer a block, describing its behaviour by a series of properties, it is not true that the verification engineer (VE) does not have as much understanding as the designer. Quite the contrary - the VE understands the code better than the designer, which is why, in my experience, the VE invariably finds bugs in this way. The reason that the VE understands the code is better is that the properties used to describe the behaviour of the implementation are at a higher-level of abstraction than the RTL. The properties draw together many strands of RTL code and express their behaviour succinctly, meaning the VE has to keep less in their head when reasoning about the code's behaviour.
This methodology is quite different from designers putting assertions into code to check implementation intent - although such assertions can indeed help this methodology. While such assertions tend to be added on an ad hoc basis, the aim here is to systematically build up a complete set of properties to describe the complete functionality of the implementation.
I think this may be a little digression from the original point of this topic. However I think it is indicative of a general point about formal techniques. Currently formal tools don't provide a magical solution to the 'verification gap'. However, if a problem-solving approach is taken to formal verification, then it gives results. If a problem-finding approach is taken, then it probably doesn't even get started, and if it does is much less likely to give results. |
|
| Back to top |
|
|
elavelle
Junior
Joined: Jun 15, 2004
Posts: 9
|
| Posted: Tue Aug 31, 2004 4:45 am Post subject: |
|
|
Hi Alex & Confused (perhaps you should consider another name?!) -
If I understand you correctly, you're both basically saying that you can get the interesting corner cases just by looking at the spec, and without any knowledge of the implementation. The verification engineer therefore doesn't need to know anything about the RTL.
If this is true, can you give me a verification plan for a 64-bit adder? Or a 32x32 multiplier? What are the interesting corner cases for these two examples? For the simple case of the adder, what corner cases would determine whether or not the carry functionality is working? And if the answer is formal verification, can your tool handle multipliers?
Yes, I agree that a functional spec is enough in many cases, but it depends on what you're verifying. Sometimes you need to have at least a limited understanding of the implementation.
Cheers
Evan |
|
| Back to top |
|
|
confused
Senior
![]()
Joined: Jan 09, 2004
Posts: 185
|
| Posted: Tue Aug 31, 2004 6:57 pm Post subject: |
|
|
| elavelle wrote: |
If I understand you correctly, you're both basically saying that you can get the interesting corner cases just by looking at the spec, and without any knowledge of the implementation. The verification engineer therefore doesn't need to know anything about the RTL.
|
I do not know the answer. Before getting to interesting corner cases, many verification engineers would cover basic test cases first by looking at the spec. If the project can afford more effort, interesting corner cases are certainly good. It is hard to make such decisions because people normally verify huge designs now. There is no limit how many interesting corner cases should be applied for a design of many million gates. There is just no "trivial" ways to verify such large designs. Many projects can only afford to cover basic test cases.
As Alex implied, design engineers should be responsible for these interesting corner cases (or assertions, depending on the methodology). They should take this part of verification responsibilities. If they do not have enough time, some verification engineers can fill the gap. When design engineers have even less time, these verification engineers can also fix/rewrite/write RTL code for them.
For some designs or some parts of a design, it is more efficient for the verification to follow a white box approach. In such cases, the spec (or other documents) can include some implementation details.
A more recent way to use design engineers' knowledge in verification is to use coverage data. If they see some significant coverage issue with the basic test cases, then verification engineers work with the implementation details to find interesting corner cases. |
|
| Back to top |
|
|
alexg
Senior
![]()
Joined: Jan 07, 2004
Posts: 586
Location: Ottawa
|
| Posted: Wed Sep 01, 2004 5:39 pm Post subject: |
|
|
Hi Evan,
please see my comments below.
| Quote: | If I understand you correctly, you're both basically saying that you can get the interesting corner cases just by looking at the spec, and without any knowledge of the implementation. The verification engineer therefore doesn't need to know anything about the RTL.
|
I would divide interesting corner cases by functional (can get their definitions from spec, example: maximum packet sizes, protocol error scenarios etc) and implementational, which, by the definition, have to be derived from implementation. By defining white-box coverage metrics, designer actually defines "implementational" corner test cases.
| Quote: | If this is true, can you give me a verification plan for a 64-bit adder? Or a 32x32 multiplier? What are the interesting corner cases for these two examples? For the simple case of the adder, what corner cases would determine whether or not the carry functionality is working? And if the answer is formal verification, can your tool handle multipliers?
|
I don't think 64-bit adder or similar blocks are good examples. They contain datapath only, without control logic. Formal tools will fail here, since adder contains large number of inputs and state variables. However, there are symbolic simulators, which may verify this block within single simulation run.
In general, I am not pretenting to give solution for all the cases. There are different ways to achieve verification goals and especially to set verification requirements. The art of verification is in choosing the most effective ways.
The main idea I an trying to formulate is:
There is no reason to do design, and then do verification. It is the same as, for example, build a deck, and then starting to compare building plan with what is already done. The price of such approach may be too high.
Formal tools are nothing more than a measurement instrument for designers, which they can use to check the code-under-development against the features defined in Spec.
Regards,
Alexander Gnusin |
|
| Back to top |
|
|
alain94040
Senior
Joined: Jun 03, 2004
Posts: 22
Location: San Jose
|
| Posted: Wed Sep 01, 2004 7:58 pm Post subject: |
|
|
| Quote: | | "Before getting to interesting corner cases, many verification engineers would cover basic test cases first by looking at the spec. If the project can afford more effort, interesting corner cases are certainly good". |
I agree and this is what I used to do.
Step 1: the Verification Engineer reads the specs and comes up with what he thinks are interesting corner cases (even though I like to rephrase this as defining coverage spaces).
Step 2: I let the Design Engineer do a presentation of his block and how it was designed. During that presentation, the Verification Engineer refines his test plan. Like "Oh, you mean you put a 10-deep FIFO between these two streams? Maybe I should check conditions around that magic 10 number then". Or "I notice you are presenting how you handle mode A a certain way. Then you present how you handle mode B. Can both modes happen simultaneously? How do you switch between the two?".
A critical mind is what you want in a Verification Engineer: listen to everything the designer says, focused on finding the hole, gap, bug, oversight, etc...
Alain Raynaud
Technical Director, EVE-USA |
|
| Back to top |
|
|
confused
Senior
![]()
Joined: Jan 09, 2004
Posts: 185
|
| Posted: Sun Sep 05, 2004 3:38 am Post subject: |
|
|
It also depends on a project's verification planning process.
If the process is rather formal, the design/spec documents are usually big, and the corresponding verification plan is also a big book. The project team have many review rounds of these documents until everybody is pretty tired of such discussions. Now the verification plan is pretty solid from a high level point of view. The amount of verification work in the plan more or less matches the verification budget. Then any significant analysis of more design details during verification by verification engineers can be seen as screwing up the priorities and the schedule.
If the process is less formal, the verification planning lists only the high level work items. Then the management only tracks how many of these items are done. Each item is assigned to a verification engineer or a small team of them. A key pressure to each of them is to show good progress. Another key issue is how to explain if some problem like the Pentium bug escapes from your item. In addition to work as hard as possible, a normal trick is to follow the "normal practice" of the verification team. Because such escapes are always possible, it is better for the whole team to share the blame. It is harder to fire the whole team (or the most respected members of the team who define the normal practice). Unless the verification team is evenly strong, the normal practice probably does not include too much analysis of design details.
Are there any other typical situations? Both of the above situations seem to encourage only a balanced level of design knowledge in verification engineers. A larger verification team does not imply a higher level of such knowledge of design details because it often implies more junior engineers in the verification team. The high percentage of junior members requires spreading senior members thinner across more design blocks, which gives them less time to analyze design details. |
|
| 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
