Abstract property verifier based on multiway decision graphs
Symbolic model-checking tools encounter state-explosion problem when verifying designs with large data paths. Multiway Decision Graph (MDG) model-checker uses abstract data representation and applies abstract operations to address the state explosion problem. The MDG verification tool, also known as...
| Main Author: | |
|---|---|
| Format: | Others |
| Published: |
2007
|
| Online Access: | http://spectrum.library.concordia.ca/975629/1/MR40883.pdf Hussain, Kamran <http://spectrum.library.concordia.ca/view/creators/Hussain=3AKamran=3A=3A.html> (2007) Abstract property verifier based on multiway decision graphs. Masters thesis, Concordia University. |
| Summary: | Symbolic model-checking tools encounter state-explosion problem when verifying designs with large data paths. Multiway Decision Graph (MDG) model-checker uses abstract data representation and applies abstract operations to address the state explosion problem. The MDG verification tool, also known as Abstract Verifier, takes as input the specification (written as properties) and the description of the design, and then proves or disproves if the design satisfies these properties. The original specification language of the Abstract Verifier was called L mdg that provides temporal operators and abstract data types to formalize properties. Meanwhile, the Property Specification Language (PSL) has changed the verification world by introducing very rich temporal operators but without abstract data types. In this thesis, we propose a new specification language called Abstract Property Language (APL), for the MDG model-checker. This language replaces the L mdg specification language by introducing new operators borrowed from PSL to improve its expressiveness. We provide the formal definition of this language in BackusNaur form (BNF) and provide its formal semantics based on the computational model of the Abstract Verifier. APL is associated with a front-end translator that accepts APL specifications and builds verification-ready models to be handled directly inside the MDG model-checker. Finally, we have validated our APL language and the translator tool on the verification of several test benches including Look-Aside Interface (LA-1) design. |
|---|