|
| |
|
| The following three designer-oriented tasks improve baseline RTL block quality by establishing basic functional sanity; identifying sources of “x” and eliminating undesired propagation; and verifying register operations. Together, they reduce overall engineering effort by allowing RTL designers to debug their own code, reducing downstream verification effort. |
|
|
|
|
- Incremental RTL development and verification: RTL is written incrementally, and ideally design changes could be effectively tracked and verified incrementally, guaranteeing against unintended side-effects of changes. The cost of uncovering a design bug increases non-linearly down the design flow. Formal verification can start with partial RTL, before testbenches are available, can aid RTL development productivity, and can effectively and incrementally verify design changes.
- Automatic register verification: Control and status registers (CSR) are the interface between software and hardware. Register verification is extremely important because a wrongly implemented CSR always breaks downstream functionality, and an implementation bug can make debugging a functional failure difficult. Formal technology converts the CSR specification is into a set of properties capturing the conditions in which the control registers can be configured, the conditions in which the control registers should maintain stable values, and the conditions in which the status registers should receive a specified value. Formal verification can then verify that these conditions are met in all cases, and simplify the debugging process of other failures.
- X-propagation detection: Certain coding styles may require designers to assign X (unknown) in RTL, and yet, if not treated properly, RTL code and gate level simulation can potentially mismatch. Unlike traditional simulation tests, which do not guarantee coverage for Xs, formal verification can exhaustively verify X propagation, proving that X's are not propagated to critical areas, and are blocked by appropriate blocking conditions.
|
|
|
|
|
|
