Font Size: a A A

Verification Of ATM Fabric's Behavior Using SPIN

Posted on:2007-02-03Degree:MasterType:Thesis
Country:ChinaCandidate:X J WuFull Text:PDF
GTID:2178360182493963Subject:Computer software and theory
Abstract/Summary:PDF Full Text Request
In recent years, Model checking has emerged as an alternative approach to ensuring the quality and correctness of hardware design, overcoming some of the limitations of traditional validation techniques such as simulation and testing. Because exhaustive testing for nontrivial designs is generally infeasible, testing provides at best only a probabilistic assurance. There are two main aspects to the application of model checking in a design process: the formal framework used to specify desired properties of a design and the verification techniques and tools used to reason about the relationship between a specification and corresponding implementation. Model checking uses rigorous mathematical reasoning to show that a design meets all or parts of specification. Typically, the user provides a high level representation of the model and the specification to be checked. The model checker will either terminate with the answer true, indicating that the model satisfies the specification, or give a counterexample execution that shows why the formula is not satisfied.This paper give a brief introduction of formal methods at first, then mainly introduce the theory and concepts of Model Checking (including CTL~*, CTL, LTL, Kripe structure etc.) and I introduced the Model Checker named SPIN and the language PROMELA accepted by SPIN.At last I investigated hardware implementation of Cambridge Fairisle Asynchronous Transfer Mode (ATM) 4 by 4 switch fabric's high-level behavioral specification which has no restrictions with respect to cell length or word width. The verification is based on the model created by PROMELA. PROMELA is a language accepted by SPIN that is a famous Model Checker. The verification is based on the reachability analysis of the product machine of the implementation and the specification. I verified some LTL properties (including liveness property and safety property) of the ATM Fairisle Switch using by SPIN.
Keywords/Search Tags:formal methods, liveness property, safety property, SPIN Model Checker, Promela language, BDD, ROBDD
PDF Full Text Request
Related items