NDLI: Axiomatic semantics of a hardware specification language

Content Provider	IEEE Xplore Digital Library
Author	Xin Hua Hantao Zhang
Copyright Year	1992
Description	Author affiliation: Dept. of Comput. Sci., Iowa Univ., Iowa City, IA, USA (Xin Hua; Hantao Zhang)
Abstract	Formal hardware design verification is to examine whether a structural specification of a circuit meets its behavioral specification. Despite the progress in formal verification, there is a big gap between hardware designers and verifiers, partially because there are no common specification languages for them to use. The authors show that formal semantics could bridge such a gap. By providing an axiomatic semantics to an existing hardware design language called the Iowa logic specification language (ILSL), the authors show that a circuit description in ILSL can be automatically converted into a set of first-order formulas which is the semantic description of the circuit and is acceptable by an existing theorem prover called the rewrite rule laboratory (RRL). In particular, they show how iterative statements of ILSL are converted into recursive functions of RLL. Their work thus results in a uniform specification language in which both hardware design and automatic verification can be done.
Starting Page	183
Ending Page	190
File Size	510781
Page Count	8
File Format	PDF
ISBN	0818626100
DOI	10.1109/GLSV.1992.218347
Language	English
Publisher	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Publisher Date	1992-02-28
Access Restriction	Subscribed
Rights Holder	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Subject Keyword	Hardware Specification languages Bridge circuits Formal verification Signal design Computer science Cities and towns Logic design Logic circuits Laboratories
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