Equivalence checking for compiler transformations in behavioral synthesis

Behavioral synthesis entails application of a sequence of transformations to compile a high-level description of a hardware design (e.g., in C/C++/SystemC) into a Register-Transfer Level (RTL) implementation. We present a scalable equivalence checking framework to validate the correctness of compile...

Full description

Saved in:
Bibliographic Details
Main Authors: Zhenkun Yang, Kecheng Hao, Kai Cong, Ray, Sandip, Fei Xie
Format: Conference Proceeding
Language:English
Subjects:
Algorithms
behavioral synthesis
Cognition
Complexity theory
Concrete
Equivalence checking
Hardware
Manuals
Semantics
transformation
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:Behavioral synthesis entails application of a sequence of transformations to compile a high-level description of a hardware design (e.g., in C/C++/SystemC) into a Register-Transfer Level (RTL) implementation. We present a scalable equivalence checking framework to validate the correctness of compiler transformations employed by behavioral synthesis. Our approach is based on dual-rail symbolic simulation of the input and output design representations of a transformation. We have evaluated our framework on transformations applied to several designs by an open source behavioral synthesis tool, and we present initial results demonstrating the approach.
ISSN:1063-6404
2576-6996
DOI:10.1109/ICCD.2013.6657090