Title :
Formal verification based on assume and guarantee approach: a case study
Author :
Roy, Subir K. ; Iwashita, Hiroaki ; Nakata, Tsuneo
Author_Institution :
Fujitsu Labs. Ltd., Kawasaki, Japan
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.
Keywords :
audio signal processing; directed graphs; finite state machines; formal verification; logic partitioning; multimedia systems; assume-guarantee approach; audio output interface subsystem; compositional verification approach; formal verification; large design verification; module level; multimedia interface subsystem; partitioning; state transition graph; system on chip design; Art; Computer aided software engineering; Design automation; Explosions; Formal verification; Hardware design languages; Laboratories; Logic; Refining; State-space methods;
Conference_Titel :
Design Automation Conference, 2000. Proceedings of the ASP-DAC 2000. Asia and South Pacific
Conference_Location :
Yokohama, Japan
Print_ISBN :
0-7803-5973-9
DOI :
10.1109/ASPDAC.2000.835074
