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.

Date

2015

Authors

Arash Saifhashemi, Hsin-Ho Huang, Priyanka Bhalerao, Peter A Beerel

Conference

2015 Design, Automation & Test in Europe Conference & Exhibition (DATE)

Pages

1563-1566

Publisher

IEEE