SISCO: Selective Invariant Sharing, Clustering and Ordering for Effective Multi-Property Formal Verification
Sourav Das, Aritra Hazra, Pallab Dasgupta, Himanshu Jain, Sudipta Kundu · 2025
Multi-property formal verification remains a significant challenge in the chip design industry. With hundreds of property goals to verify in a design, several questions arise regarding goal ordering and grouping of properties, sharing of information across proven properties, and other heuristics to improve the verification productivity. This paper introduces SISCO, a novel method for addressing multi-property verification in complex designs. SISCO unfolds properties to a certain depth, clusters them, reorders properties within each cluster, and then uses a modified version of IC3/Property Directed Reachability (PDR) algorithm for efficient verification. The method stores the invariants of proven properties and selectively shares them while solving undecided goals. Additionally, SISCO keeps track of counter-example traces of falsified goals to assist verification. Experimental results demonstrate that clustering and ordering help solve more goals while selective invariant sharing accelerates the process. SISCO achieves a significant average improvement of 4.73× in the runtime of individual goals compared to all invariant sharing.