Error Diagnosis in Equivalence Checking of High Performance Microprocessors
Alper Şen · Electronic Notes in Theoretical Computer Science · 2007
We describe techniques for diagnosing errors in formal equivalence checking of RTL and transistor level models of high performance microprocessors at Freescale Semiconductor Inc. We use Symbolic Trajectory based Evalaution (STE) for combinational equivalence checking. STE accurately captures transistor level behaviors. We use simulation based error diagnosis techniques and present a seamless integration of them in our current verification environments.