Sciweavers

TCAD
2008

Application and Verification of Local Nonsemantic-Preserving Transformations in System Design

13 years 10 months ago
Application and Verification of Local Nonsemantic-Preserving Transformations in System Design
Due to the increasing abstraction gap between the initial system model and a final implementation, the verification of the respective models against each other is a formidable task. This paper addresses the verification problem by proposing a stepwise application of combined refinement and verification activities in the context of synchronous model of computation. An implementation model is developed from the system model by applying predefined design transformations which are as follows: 1) semantic preserving or 2) nonsemantic preserving. Nonsemantic-preserving transformations introduce lower level implementation details, which are necessary to yield an efficient implementation. Our approach divides the verification tasks into two activities: 1) the local correctness of a refined block is checked by using formal verification tools and predefined properties, which are developed for each nonsemantic-preserving transformation, and 2) the global influence of the refinement to the entire ...
Tarvo Raudvere, Ingo Sander, Axel Jantsch
Added 15 Dec 2010
Updated 15 Dec 2010
Type Journal
Year 2008
Where TCAD
Authors Tarvo Raudvere, Ingo Sander, Axel Jantsch
Comments (0)