em04_danka

A Formal Verification Methodology for IP-based Designs

Daniel Karlsson Author homepage
 
Petru Eles Author homepage
Zebo Peng Author homepage

EUROMICRO SYMPOSIUM ON DIGITAL SYSTEM DESIGN, Architectures, Methods and Tools, Rennes, France, August 31-September 3, 2004, pp 372-379.

ABSTRACT
This paper proposes a formal verification methodology which smoothly integrates with component-based system-level design, using a divide and conquer approach. The methodology assumes that the system consists of several reusable components, each of them already verified by their designers and which are considered correct under the assumption that the environment satisfies certain properties assumed by the component. What remains to be verified is the glue logic inserted between the components. Each such glue logic is verified one at a time using model checking techniques. Experiments, performed on a real-life example (mobile telephone), demonstrating the efficiency and intuitivity of the methodology, are moreover thoroughly presented. Three different properties have been verified on one part of the system.


Related files:
em04_danka.pdfAdobe Acrobat portable document


[KEP04] Daniel Karlsson, Petru Eles, Zebo Peng, "A Formal Verification Methodology for IP-based Designs", EUROMICRO SYMPOSIUM ON DIGITAL SYSTEM DESIGN, Architectures, Methods and Tools, Rennes, France, August 31-September 3, 2004, pp 372-379.
( ! ) perl script by Giovanni Squillero with modifications from Gert Jervan   (v3.1, p5.2, September-2002-)
Last modified on Monday December 04, 2006 by Gert Jervan