학술논문

Formal verification based on assume and guarantee approach: a case study
Document Type
Conference
Source
Proceedings 2000. Design Automation Conference. (IEEE Cat. No.00CH37106) Asia and South Pacific design automation conference 2000 Design Automation Conference, 2000. Proceedings of the ASP-DAC 2000. Asia and South Pacific. :77-80 2000
Subject
Computing and Processing
Communication, Networking and Broadcast Technologies
Components, Circuits, Devices and Systems
Formal verification
Computer aided software engineering
Refining
State-space methods
Hardware design languages
Laboratories
Explosions
Logic
Design automation
Art
Language
Abstract
In this paper, we present a verification case study of the Audio Output Interface (AOF) subsystem based on a compositional verification approach known as the Assume-Guarantee approach. We illustrate how designers can leverage their detailed knowledge of a design to partition it at the module level, and, thereby, enable the Assume-Guarantee approach to overcome intrinsic limitations of a formal verification tool to successfully verify large designs.