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

fYear

2000

fDate

9-9 June 2000

Firstpage

77

Lastpage

80

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;

fLanguage

English

Publisher

ieee

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

Type

conf

DOI

10.1109/ASPDAC.2000.835074

Filename

835074