| 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 |
dave_whipp
Senior
Joined: Jan 06, 2004
Posts: 76
Location: Santa Clara, CA
|
 Posted: Thu Oct 21, 2004 11:23 am Post subject: |
 |
|
Nice question, j. It should help us too see houw (and if) our definitions really differ.
I think that answer is that you can do it either way. My 1st reaction (which might change if I think about it a bit more) is that the key is how we deal wioth the routing table itself.
To my mind, if I were implementing a "checker" approach, then I would create a checker that uses the rtl's implementation of the routing table (maybe via a backdoor access to its memory representation) to determine where a given packet should emerge; and then create a checker that checks the property that the packet should be routed to where the table says it should be. (This ignores the fact that it might later be culled to manage bandwidth). A separate checker would monitor the integrity of the routing table itself.
If I was to check this using a modeling approach, then the model would maintain its own representation of the routing table, and would use that representation to determine where the packet should go, and thus would be susceptible to the interactions between updates and searches.
The difference between the two approaches is not huge. In both cases we need to create non-rtl code that predicts the behavior of updates to the routing table; and in both we need code that uses routing table information to predict where a packet should be routed.
The main difference in my mind is that by combining them into a single model, we gain the ability to validate interactions between the two without running the RTL -- which may enable more comprehensive validation of the interactions due to facter simulation speeds.
Another interesting side effect of using the model is that it may enable our regressions to run faster. Each point that you monitor in the RTL may slow down your simulations, because the simulator's optimizer is constrained by the need to provide acess tothe signal. If the existence of an end-to-end model allows us to omit a significant number of internal monitoring points without a significant loss of coverage, then we may be able to increase the size of out regression suite: and only turn on all the checkers when an end-to-end check fails. If the verification approach is entirely one of independent single-property checkers, then removal of an internal checker wil reduce coverage. This effect can be particularly noticable on emulation, where the IO demands of dumping too many internal signals becomes a significant overhead.
Dave. |
|
| Back to top |
|
 |
alexg
Senior
![]()
Joined: Jan 07, 2004
Posts: 586
Location: Ottawa
|
| Posted: Thu Oct 21, 2004 3:36 pm Post subject: |
|
|
| jmcneal wrote: |
For any complex property/function that needs to be verified on a large chip, isn't it often necessary to use a model in order to perform checking?
|
In fact, it is sometimes difficult to distinguish between checker and model, as well as between implementation and specification code. Dave provided another example - square root function. Is it a function or property? Both, actually.
To provide more precise answer on this question, I would like first to quickly describe chip design/verification process as I understand it.
In short, it can be desribed as:
properties <-verification-> algorithms <-verification-> implementation
Most designs start from the initial idea(s), which are actually properties. In order to prove the concept of the chip, there is a need for high-level modeling. This modeling belongs to architectural stage, and the outcome of it is the confidence that it is possible to develop design which will suit all the funcitonal and backend constraints.
Then, Specification document is written. In most cases, it contains as properties definitions, as implementation details or algorithms which are the outcome of architectural modeling phase - structural and FSM drawings, lines of algorithm code etc.
Note, that high-level modeling also require high-level verification against the set of initially defined properties. This is actually the ideal task for the formal property checking, since in most cases implementations, being high-level and partial, can be easily fit into the formal tools and properties can be verified exhaustively against the algorithms/FSMs.
Verification engineers, in majority of cases, don't participate in this part of verification; this is very unfortunate, since the cost of specification bugs is very high.
Usually, verification task as we understand it starts when Speicification document is published. Since it contains the mix of properties and partial implementation definitions, verification approach may be not clear. There are actually two main parts in it:
1. Verify Specification properties against implementation code.
2. Verify partial high-level implementation (algorithms) defined in Spec agains implementation code.
The first part, IMHO, is the most important one. Even if we'll not verify exactly the algorithm proposed in Spec, implementation still may function properly once all the properties are verified. Checkers/Constraint-Random Stims/Coverage points are really useful tools for the properties verification
The second part requires the modeling approach. In this case, we may define checkers as a models plus comparing/report generation logic, and still stay within checker-based methodology.
As I understand, you are verifying rooting/switching algorithm, and this algorithm is defined in Specification document. Algorithm is not a property, so if you don't trust designers you'll have to re-implement it as is in another way and then compare with implementation logic. However, it is extremely important to independently check the properties of any given algorithm, even the one copied from specification. For example, you may think about such properties as packets starvation, fairness of priority arbitration, throughput and link utilization for any traffic patterns etc.
Regards,
Alexander Gnusin |
|
| 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
