NDLI: Equivalence Checking of Datapaths Based on Canonical Arithmetic Expressions

Content Provider	IEEE Xplore Digital Library
Author	Zheng Zhou, Wayne Burleson
Copyright Year	1995
Description	Author affiliation: Department of Electronic & Computer Engineering, University of Massachusetts at Amherst, MA (Zheng Zhou, Wayne Burleson)
Abstract	Numerous formal verification systems have been proposed and developed for Finite Sate Machine based control units (notably SMV[19] as well as others). However, most research on the equivalence checking of datapaths is still confined to the bit-level. Formal verification of arithmetic expressions and synthesized datapaths, especially considering finite word-length computation, has not been addressed. Thus formal verification techniques have been prohibited from more extensive applications in numerical and Digital Signal Processing. In this paper a formal system, called Conditional Term Rewriting on Attribute Syntax Trees (ConTRAST) is developed and demonstrated for verifying the equivalence between two differently synthesized datapaths. This result arises from a sophisticated integration of attribute grammars, which provide expressive data structures for syntactic and semantic information about designed datapaths, and term rewriting systems, which transform functionally equivalent datapaths into the same canonical form. The equivalence relation is defined as a congruence closure in the rewriting system, which can be generated from arbitrary axioms, such as associativity, commutativity, etc. in a certain algebraic system. Furthermore, the effect of finite word-lengths and their associated arithmetic precision are also considered in the definition of equivalence classes. As a particular application of ConTRAST, a formal verification system is designed to check equivalence under precision constraints. The results of initial DSP synthesis experiments are displayed, where two differently implemented IIR filters in direct II and cascaded architectures are automatically compared under given precision constraints.
Starting Page	546
Ending Page	551
File Size	237855
Page Count	6
File Format	PDF
ISBN	0897917251
ISSN	0738100X
DOI	10.1109/DAC.1995.250007
Language	English
Publisher	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Publisher Date	1995-06-12
Publisher Place	USA
Access Restriction	Subscribed
Rights Holder	Association for Computing Machinery, Inc. (ACM)
Subject Keyword	Control system synthesis Data structures Digital arithmetic Signal synthesis Digital signal processing Boolean functions Control systems Commutation Automatic control Signal processing algorithms System-Level Design Aids Design Verification High-Level Synthesis
Content Type	Text
Resource Type	Article

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