doi: 10.7873/DATE.2015.0299

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)