Title :
Formal analysis of hardware requirements
Author :
Pill, I. ; Semprini, S. ; Cavada, R. ; Rovers, Madelon ; Bloem, R. ; Cimatti, A.
Author_Institution :
Graz Univ. of Technol.
Abstract :
Formal languages are increasingly used to describe the functional requirements (specifications) of circuits. These requirements are used as a means to communicate design intent and as basis for verification. In both settings it is of utmost importance that the specifications are of high quality. However, formal requirements are seldom the object of validation, even though they can be hard to understand and interactions between them can be subtle. In this paper, we present techniques and guidelines to explore and assure the quality of a formal specification. We define a technique to interactively explore the semantics of a specification by simulating its behavior for user-defined scenarios. Furthermore, we define techniques to automatically check specifications against a set of user-provided assertions, which must be satisfied, and a set of possibilities, which must not be contradicted. The proposed techniques support the user in the iterative development and refinement of high-quality specifications
Keywords :
electronic design automation; formal specification; formal verification; programming language semantics; systems analysis; formal languages; formal specification; formal verification; functional specifications; hardware design; requirement analysis; semantics; specifications checking; Analytical models; Circuits; Formal languages; Formal specifications; Guidelines; Hardware; Natural languages; Specification languages; Writing; Hardware Design; Property Assurance; Property Simulation; Requirements Analysis; Specification;
Conference_Titel :
Design Automation Conference, 2006 43rd ACM/IEEE
Conference_Location :
San Francisco, CA
Print_ISBN :
1-59593-381-6
DOI :
10.1109/DAC.2006.229231