Accellera Systems Initiative is an independent, not-for profit organization dedicated to create, support, promote, and advance system-level design, modeling, and verification standards for use by the worldwide electronics industry. We are composed of a broad range of members that fully support the work of our technical committee to develop technology standards that are balanced, open, and benefit the worldwide electronics industry. Leading companies and semiconductor manufacturers around the world are using our electronic design automation (EDA) and intellectual property (IP) standards in a wide range of projects in numerous application areas to develop consumer, mobile, wireless, automotive, and other “smart” electronic devices. Through an ongoing partnership with the IEEE, standards and technical implementations developed by Accellera Systems Initiative are contributed to the IEEE for formal standardization and ongoing governance.

1114: Liveness Assume-Guarantee Proof Schema: A step towards Liveness Full Proofs

Wednesday, March 6, 2024 3:00 pm — 4:30 pm

Formal Verification (FV) has established itself as a critical element of high-quality functional verification, playing an indispensable role in the success of tape-out of modern hardware designs. While safety properties have received significant attention in recent EDA tool advancements, liveness properties remain relatively overlooked, even among formal experts. In this work, we introduce a robust mathematical formulation aimed at delving into exploring deep states in the design and uncover liveness issues like starvation, livelocks, and deadlocks etc. Furthermore, we extend this methodology to break down the FV complexity related to liveness, enabling us to achieve exhaustive proofs for liveness properties. We also present the bugs found by this approach in multiple DV signed off designs.