doi: 10.3850/978-3-9815370-4-8_0299

Logical Equivalence Checking of Asynchronous Circuits using Commercial Tools

Arash Saifhashemi¹, Hsin-Ho Huang^2,a, Priyanka Bhalerao³ and Peter A. Beerel^2,b

¹Intel Corporation, Santa Clara, CA, USA.

saifhash@usc.edu

²Electrical Engineering, University of Southern California, Los Angeles, CA, USA.

^ahsinhohu@usc.edu ^bpabeerel@usc.edu

³Yahoo Corporation, Sunnyvale, CA, USA.

pbhalera@usc.edu

ABSTRACT

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)

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.

ABSTRACT

Arash Saifhashemi¹, Hsin-Ho Huang^2,a, Priyanka Bhalerao³ and Peter A. Beerel^2,b

¹Intel Corporation, Santa Clara, CA, USA.

²Electrical Engineering, University of Southern California, Los Angeles, CA, USA.

³Yahoo Corporation, Sunnyvale, CA, USA.