Logical Equivalence Checking of Asynchronous Circuits using Commercial Tools
Arash Saifhashemi1, Hsin-Ho Huang2,a, Priyanka Bhalerao3 and Peter A. Beerel2,b
1Intel Corporation, Santa Clara, CA, USA.
2Electrical Engineering, University of Southern California, Los Angeles, CA, USA.
3Yahoo Corporation, Sunnyvale, CA, USA.
We propose a method for logical equivalence check (LEC) of asynchronous circuits using commercial synchronous tools. In particular, we verify the equivalence of asynchronous circuits which are modeled at the CSP-level in SystemVerilog as well as circuits modeled at the micro-architectural level using conditional communication library primitives. Our approach is based on a novel three-valued logic model that abstracts the detailed handshaking protocol and is thus agnostic to different gate-level implementations, making it applicable to a variety of different design styles. Our experimental results with commercial LEC tools on a variety of computational blocks and an asynchronous microprocessor demonstrate the applicability and limitations of the proposed approach.
Full Text (PDF)