It is a challenging problem to formally verify mathematical datapath designs. Such designs, by nature, do not lend themselves well to be verified via traditional model checking algorithms. However, formal transactional equivalence checking with a “golden” reference model can be used successfully to verify datapath designs. In this paper, we describe how we used HECTOR – a C-vs-RTL transactional equivalence checking tool from Synopsys – to formally establish the correctness of a multiplier design for an X86 processor core. We also used the Synopsys VC Formal tool to prove correctness of a complex divider design. The transactional equivalence checking was repeated several times as the designs went through changes to satisfy power and performance requirements. Due to the large complexity in the designs, we pushed the limits and had deployed various recipes and techniques, including transitivity and assume-guarantee.
