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

Content Provider	IEEE Xplore Digital Library
Author	Karfa, C. Sarkar, D. Mandal, C.
Copyright Year	1982
Abstract	A formal verification method of the datapath and controller generation phase of a high-level synthesis (HLS) process is described in this paper. The goal is achieved in two steps. In the first step, the datapath interconnection and the controller finite state machine description generated by a high-level synthesis process are analyzed to obtain the register transfer-operations executed in the datapath for a given control assertion pattern in each control step. In the second step, an equivalence checking method is deployed to establish equivalence between the input and the output behaviors of this phase. A rewriting method has been developed for the first step. Unlike many other reported techniques, our method is capable of validating pipelined and multicycle operations, if any, spanning over several states. The correctness and complexity of the presented method have been treated formally. The method is implemented and integrated with an existing HLS tool, called structured architecture synthesis tool. The experimental results on several HLS benchmarks indicate the effectiveness of the presented method.
Sponsorship	IEEE Council on Electronic Design Automation IEEE Circuits and Systems Society
Starting Page	479
Ending Page	492
Page Count	14
File Size	497951
File Format	PDF
ISSN	02780070
Volume Number	29
Issue Number	3
Language	English
Publisher	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Publisher Date	2010-03-01
Publisher Place	U.S.A.
Access Restriction	One Nation One Subscription (ONOS)
Rights Holder	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Subject Keyword	High level synthesis Digital circuits Computer bugs Formal verification Automata Scheduling Control system synthesis Signal synthesis Integrated circuit interconnections Pattern analysis register transfer level Controller datapath equivalence checking formal verification FSM FSMD models high-level synthesis
Content Type	Text
Resource Type	Article
Subject	Computer Graphics and Computer-Aided Design Electrical and Electronic Engineering Software

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

Formal Verification of Behavioural Transformations during Embedded System Design

On the efficiency of formal synthesis-experimental results

Sequential equivalence checking based on structural similarities

Sequential Equivalence Checking for Clock-Gated Circuits

Relative scheduling under timing constraints: algorithms for high-level synthesis of digital circuits

Formal Methods for Aiding Verification of Local Design Changes in Digital Integrated Circuits

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

Equivalence Checking of System-Level and SPICE-Level Models of Linear Circuits

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

Similar Documents

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

Formal Verification of Behavioural Transformations during Embedded System Design

On the efficiency of formal synthesis-experimental results

Sequential equivalence checking based on structural similarities

Sequential Equivalence Checking for Clock-Gated Circuits

Relative scheduling under timing constraints: algorithms for high-level synthesis of digital circuits

Formal Methods for Aiding Verification of Local Design Changes in Digital Integrated Circuits

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

Equivalence Checking of System-Level and SPICE-Level Models of Linear Circuits

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