|
|
|
| |
|
Architectural formal verification involves verifying the design architecture described in SystemVerilog against the set of specifications. Typically, this takes place prior to any RTL coding stage. Uncovering architecture-related problems in the early stage prevents costly downstream re-designs. For example, it’s practically infeasible to get sufficient coverage at the design level for cache-coherence protocol checking. There are four main categories of architectural verification:
|
|
|
|
|
- Communication protocol: A communications protocol is the set of standard rules for data representation, signaling, authentication and error detection required to send information over a communications channel. Formal property language provides a precise medium for capturing these rules, and formal verification can verify the soundness and completeness of the rules, and expose subtle synchronization flaw in the protocol.
- Cache coherency protocol: A cache-coherence protocol contains complex interactions with parallelism and multi-threading. To verify a cache-coherence protocol, a tool must consider a range of traces that are both wide (in terms of starting and branching points) and deep (with long sequences of events). That’s hard enough with an architectural model and infeasible with a design level model. With complex protocols, it becomes extremely difficult to determine which corner cases are possible and how they might be manifested. Formal verification is well suited at discovering these corner cases in the protocol, and can provide architects with an executable specification that can be queried.
- Architectural liveness: Architectural verification is on critical path because the consequences of an undetected architectural bug are so severe. RTL verification won’t catch such a bug; it will simply show that the RTL code matches the architectural spec. An architectural specification bug may well remain undetected until silicon, causing time-to-market delays, redesign, and possibly a silicon respin. Furthermore, liveness verification, i.e. checking that something defined as “good” eventually happens according to the architecture, is also extremely important.
- Power architecture: Low-power designs often utilitize CPF or UPF to specify the desired power architecture, providing an easy-to-use, easy-to-modify specification of power intent throughout the flow: design, verification, and implementation. Such information, plus temporal behavior controlled by the power management unit, can be converted into appropriate properties for formal verification, allowing automation and exhaustive analysis, and debug of the power architecture.
|
|
|
|
|
|
|
|
