Formal Verification IPs

AerieLogic proposes Formal Verification IPs that target popular SoC protocols such as Amba APB / AHB / AXI or OCP 2.2 / 2.1 / 2.0 / 1.0. These Formal-VIPs work seamlessly with several major formal verification tools and simulators of the EDA market.

Formal-VIPs enable to automatically and exhaustively prove that your design is 100% compliant with the given protocol, without any need for assertions or formal verification knowledge. Best of all, these Formal-VIPs work with your favorite formal verification tool. The same Formal-VIP can also be used during simulation for additional system-level verification.

Formal-VIPs provide a GUI wizard or CLI for easy set-up, complete documentation including references to the original specification, regression script and report generation. Once the parameter file is set using the wizard, the Formal-VIP automatically creates the complete formal environment and instanciates all assertions for the targeted formal tool.

Then simply launch the regression script to prove that your design is 100% compliant with the protocol, or to automatically compute short test-sequences that illustrate the design's protocol violations. In addition to validating the protocol layer, many deep bugs and corner-cases are uncovered automatically with our Formal-VIP performance properties running at the protocol level.

 Please visit the following links for technical details:

 OCP Formal-VIP               OCP exhaustive formal protocol checking solution

 AXI Formal-VIP                 AXI/APB exhaustive formal protocol checking solution

 AHB Formal-VIP               AHB/APB exhaustive formal protocol checking solution

 I2C Formal-VIP             I2C exhaustive protocol checking solution

If you do not find your protocol listed above, please contact us at for availability of other protocols.

 

OEM Products

AerieLogic leverages its team's extensive experience in industry-oriented formal verification to propose state-of-the-art OEM products for integration by third-party EDA or CAD companies. Please visit the following links for technical details:

FV-ABV                        A complete formal verification solution for OEM

FV-RTL                         A RTL-level formal verification solution for OEM

FV-Netlist                    A low-level entry formal verification solution for OEM