Seqver : A Sequential Equivalence Verifier for Hardware Designs

This paper addresses the problem of formal equivalence verification of hardware designs. Traditional methods and tools which perform equivalence verification are commonly based on combinational equivalence verification (CEV) methods. We however present a novel method and tool (Seqver) for performing sequential equivalence verification (SEV). The theory behind Seqver is based on the alignability theory, however in this paper we present a refinement to that theory: strong alignability, which introduces a concept of automatic model synchronization to the verification process. Automatic synchronization (reset) of sequential synchronous circuits is considered as one of the most challenging tasks in the domain of sequential equivalence verification. Earlier attempts were based on BDDs or classical reachability analysis, which by nature suffer from capacity limitations. Seqver is empowered with hybrid verification engines which combine state of the art SAT and BDD based engines for performing synchronization and verification. Seqver is widely used today in Intel for formally verifying leading next generation CPU designs.