|
| |
|
| RTL block verification requires full proofs of critical functionality as the entire block or selected function is exhaustively verified. Doing so eliminates duplication by cutting down on block-level and chip-level simulation effort, and completely eliminates any corner-case issues for critical design functionality. There are five sub-applications: |
|
|
|
|
- Verifying critical functionality: Formal verification enables exhaustive verification of critical functionality, removing uncertainty on corner cases that traditional simulation with directed and constrained random tests may miss.
- Protocol certification: Formal property languages can capture protocol rules precisely in an executable format, enabling protocol certification to confirm that a piece of RTL obeys the protocol rules in all cases.
- Verifying token leakage: Token leakage is hard to detect in simulation, since its effect may not be apparent, manifesting only in performance degradation. By specify token leakage as an explicit specification-level property for formal verification, corner cases that result in token leakage can be determined and be fixed.
- Verifying packet integrity: Packet integrity is a common specification for data transport design, and although it requires great capacity in a formal verification solution, this reduces the need to verify other implementation-level properties, and achieves a higher level of return-on-investment on verification effort.
- Block-level simulation replacement: Simulation is quite time-consuming, creating block-level test benches for simulation is tedious, and maintaining them is even harder as blocks evolve. Formal verification is much faster than simulation, obviates the overhead of creating and maintaining block-level testbenches, and evolves with RTL changes, so it is a natural choice to replace simulation.
|
|
|
|
|
|
