Automatic Assertion Checking Using Formal Symbolic Model Verifier

• Main Authors: Chia-Yuan Uang, 汪加元
• Other Authors: Jing-Yang Jou
• Format: Others
• Language: en_US
• Published: 2005
• Online Access: http://ndltd.ncl.edu.tw/handle/15654269991971750495

碩士 === 國立交通大學 === 電機資訊學院碩士在職專班 === 93 === Assertion based verification (ABV) methodology has emerged as a paradigm of high-level design verification. An assertion is used to specify what is to be exercised and verified against the intended functionality. However assertions which may contain conflicts among themselves are not inspected until later simulation stage.In this thesis, we present an automatic assertion checking which utilizes an existing symbolic model verifier as a model checker to check if there is any conflict among input assertions. We propose an approach to convert the assertions into structural Deterministic Finite Automata (DFA) and their corresponding properties. Those converted DFA and properties are then checked by using formal model verifier. This approach may facilitate assertion checking to find out potential conflict in the early stage of design activities without simulation.