App for using formal methods for the verification of low power SOC designs

Jasper Design Automation has made available of its new JasperGold Low Power Verification App (JG-LPV App) which enables users to utilize formal methods for the verification of SOC designs optimized for lower power consumption with multiple voltage and power-management domains. The JG-LPV App reads the RTL description and creates an internal power-aware formal model in accordance with the power partitioning specifications. The new App verifies power optimization structures, power management circuitry, power sequencing, and works with other JasperGold Apps to verify that the power optimizations do not corrupt the original design functionality. The JG-LPV App supports the standard UPF and CPF power intent specification formats. The App’s automated approach, together with the exhaustive nature of formal verification, can reduce verification time, cost, and risk compared to traditional power-aware verification approaches. While many tools and methodologies are used for power estimation, power optimization and structural verification, JG-LPV is designed specifically to verify the correct implementation of the power intent specification and the functionality of the design after the insertion of power management circuitry. Its automation makes it critical in the verification of SOC designs, in which low-power management constructs are introduced at different phases in the SOC deve...