Architectural specifications for multi-core SOC protocols are complex, hard to design and difficult to verify. The architect must verify the inherent correctness of protocol specification and in addition show the absence of deadlocks and other meta properties. The task is made more complex because the protocol fabric (RTL) may not yet exist and the architecture is yet to be realized. The goal, then, is to capture the specification, verify the specification and leverage the verification environment in 'down stream' implementation of the SOC. Dynamic verification systems (e.g. Simulation) are inefficient because modeling the right stimuli mandated by the specifications is impractical. Such dynamic systems are also insufficient because protocol behavior is complex and non-deterministic.
The Jasper Architectural Validation solution solves these challenges by:
- Facilitating creation of an executable spec which allows visualizing and confirming protocol behavior at architectural level without any RTL or testbench
- Generating properties and RTL from the executable spec
- Leveraging protocol validation knowledge at the architectural level during RTL implementation
- Exhaustively verifying complex protocols such as the AMBA® 4 AXI Coherency Extensions (ACE) using Jasper’s powerful proof engines
JasperGold Architectural Modeling App
Jasper provides the JasperGold Architectural Modeling App as part of our JasperGold Apps Architecture that can help you in your formal property verification efforts. The JasperGold Architectural Modeling App is just one of many apps designed to help you achieve your design and verification goals
Learn more about the JasperGold Architectural Modeling App for addressing RTL development issues.
Learn more about other JasperGold Apps that can help you.