Record Details

Formal specification and verification of hardware designs

DSpace at IIT Bombay

View Archive Info
 
 
Field Value
 
Title Formal specification and verification of hardware designs
 
Creator RAMESH, S
RAO, SSSP
SIVAKUMAR, G
BHADURI, P
 
Subject pipelining
synchronous languages
formal methods
theorem proving
 
Description Designing modern processors is a great challenge as they involve millions of components. Traditional techniques of testing and simulation do not suffice as the amount of testing required is quite enormous. Design verification is an effective alternative technique for increasing the confidence in the design. Formal verification involves checking whether the system being verified behaves as per the specification using mathematical techniques. In this paper we describe some techniques for enhancing the use of formal methods for the specification and verification of hardware systems. We examine how the language Esterel can be used to specify and verify properties of pipelined microprocessors. We also discuss methods for taking hardware descriptions of simple circuits written in VHDL and automatically generating the inputs needed by a theorem prover to prove properties of the circuit.
 
Publisher SPIE-INT SOC OPTICAL ENGINEERING
 
Date 2011-10-23T17:36:05Z
2011-12-15T09:11:16Z
2011-10-23T17:36:05Z
2011-12-15T09:11:16Z
1998
 
Type Proceedings Paper
 
Identifier PHOTOMASK AND X-RAY MASK TECHNOLOGY V,3412,261-268
0-8194-2864-7
0277-786X
http://dx.doi.org/10.1117/12.328817
http://dspace.library.iitb.ac.in/xmlui/handle/10054/15190
http://hdl.handle.net/100/1955
 
Source Conference on Photomask and X-Ray Mask Technology V,KAWASAKI, JAPAN,APR 09-10, 1998
 
Language English