NDLI: Formal verification of code motion techniques using data-flow-driven equivalence checking

Content Provider	ACM Digital Library
Author	Sarkar, Dipankar Mandal, Chittaranjan Karfa, Chandan
Copyright Year	2013
Abstract	A formal verification method for checking correctness of code motion techniques is presented in this article. Finite State Machine with Datapath (FSMD) models have been used to represent the input and the output behaviors of each synthesis step. The method introduces cutpoints in one FSMD, visualizes its computations as concatenation of paths from cutpoints to cutpoints, and then identifies equivalent finite path segments in the other FSMD; the process is then repeated with the FSMDs interchanged. Unlike many other reported techniques, the method is capable of verifying both uniform and nonuniform code motion techniques. It has been underlined in this work that for nonuniform code motions, identifying equivalent path segments involves model checking of some data-flow properties. Our method automatically identifies the situations where such properties are needed to be checked during equivalence checking, generates the appropriate properties, and invokes the model checking tool NuSMV to verify them. The correctness and the complexity of the method have been dealt with. Experimental results demonstrate the effectiveness of the method.
Starting Page	1
Ending Page	37
Page Count	37
File Format	PDF
ISSN	10844309
e-ISSN	15577309
DOI	10.1145/2209291.2209303
Volume Number	17
Issue Number	3
Journal	ACM Transactions on Design Automation of Electronic Systems (TODAES)
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	2012-07-05
Publisher Place	New York
Access Restriction	One Nation One Subscription (ONOS)
Subject Keyword	FSMD models Formal verification Code motion Equivalence checking High-level synthesis Model checking
Content Type	Text
Resource Type	Article
Subject	Computer Graphics and Computer-Aided Design Computer Science Applications Electrical and Electronic Engineering

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

An Equivalence-Checking Method for Scheduling Verification in High-Level Synthesis

Data-Flow Driven Equivalence Checking for Verification of Code Motion Techniques

Verification of Datapath and Controller Generation Phase in High-Level Synthesis of Digital Circuits

Equivalence checking between behavioral and RTL descriptions with virtual controllers and datapaths

Hand-in-hand verification of high-level synthesis

Scalable SMT-Based Equivalence Checking of Nested Loop Pipelining in Behavioral Synthesis

Extending the FSMD Framework for Validating Code Motions of Array-Handling Programs

ATM switch design by high-level modeling, formal verification and high-level synthesi

Using 2-domain partitioned OBDD data structure in an enhanced symbolic simulator

Formal verification of code motion techniques using data-flow-driven equivalence checking

Similar Documents

An Equivalence-Checking Method for Scheduling Verification in High-Level Synthesis

Data-Flow Driven Equivalence Checking for Verification of Code Motion Techniques

Verification of Datapath and Controller Generation Phase in High-Level Synthesis of Digital Circuits

Equivalence checking between behavioral and RTL descriptions with virtual controllers and datapaths

Hand-in-hand verification of high-level synthesis

Scalable SMT-Based Equivalence Checking of Nested Loop Pipelining in Behavioral Synthesis

Extending the FSMD Framework for Validating Code Motions of Array-Handling Programs

ATM switch design by high-level modeling, formal verification and high-level synthesi

Using 2-domain partitioned OBDD data structure in an enhanced symbolic simulator

Formal verification of code motion techniques using data-flow-driven equivalence checking