Verification Approach of Metropolis Design Framework for Embedded Systems |
| |
Authors: | Xi Chen Harry Hsieh Felice Balarin |
| |
Affiliation: | (1) University of California, Riverside, California, USA;(2) Present address: Novas Software, Inc., San Jose, CA, USA;(3) Cadence Berkeley Laboratories, Berkeley, CA, USA |
| |
Abstract: | In this paper, we focus on the verification approach of Metropolis, an integrated design framework for heterogeneous embedded
systems. The verification approach is based on the formal properties specified in Linear Temporal Logic (LTL) or Logic of
Constraints (LOC). Designs may be refined due to synthesis or be abstracted for verification. An automatic abstraction propagation
algorithm is used to simplify the design for specific properties. A user-defined starting point may also be used with automatic
propagation. Two main verification techniques are implemented in Metropolis the formal verification utilizing the model checker
Spin and the simulation trace checking with automatic generated checkers. Translation algorithms from specification models
to verification models, as well as algorithms of generated checkers are discussed. We use several case studies to demonstrate
our approach for verification of system level designs at multiple levels of abstraction. |
| |
Keywords: | LTL LOC metropolis meta-model spin property simulation formal verification |
本文献已被 SpringerLink 等数据库收录! |
|