As the pressure to produce smaller and faster hardware designs increases, the need for formal verification of sequential transformations increases proportionally. In this talk we describe a framework that attempts to extend the set of designs that can be equivalence checked. Our focus lies in integrating sequential equivalence checking into a standard design flow that relies on combinational equivalence checking today. In order to do so, we can not make use of reset state or reset sequence information (as this is not given in combinational equivalence checking), and we need to mitigate the complexity inherent in the traditional sequential equivalence checking algorithms. Our solution integrates combinational and sequential equivalence checking in such a way that the individual analyses benefit from each other. The experimental results show that our framework can verify designs which are out of range for pure sequential equivalence checking methods aimed designs with unknown reset
Per Bjesse works on formal verification at Synopsys, and has a PhD in Computer Science from Chalmers Technical University, Sweden. He is interested in all aspects of analysis of industrial systems, ranging from hardware model checking to embedded software testing and verification.
Prof. Fei Xie