Model Checking RT-Level Hardware Systems

• Main Authors: Cheng-Yin Wu, 吳政穎
• Other Authors: Chung-Yang (Ric) Haung
• Format: Others
• Language: en_US
• Published: 2014
• Online Access: http://ndltd.ncl.edu.tw/handle/76601859990180165600

博士 === 國立臺灣大學 === 電子工程學研究所 === 102 === Model checking, or property checking, is a classic methodology for formally verifying a hardware system. More specifically, given a system and a set of properties, model checkers judge whether the system satisfies a property or not. However, due to the high complexity of model checking, as the design complexity and the number of property to be verified grows rapidly, the capability of model checking decreases. In this thesis, we present a complete framework for model checking of RT-level hardware systems. The framework consists of three major building blocks: FORMAL MODELING, PREPROCESSING, and MODEL CHECKING. Starting from FORMAL MODELING, a complicated RT-level design is parsed, synthesized, and then modeled as a word-level network. Next in the PREPROCESSING stage, rewriting and resynthesis techniques are applied to optimize the network, and moreover, property-directed constraints and invariants are extracted from design abstraction for improving model checking. After properties are elaborated at the end of PREPROCESSING, a portfolio-based model checker starts to verify all the properties in the MODEL CHECKING stage, and in particular, different model checking algorithms share information (e.g. deep bounds and reachabilities) on-the-fly to complement each other. Our experimental evaluation shows that our framework, equipped with abovementioned techniques, is capable of model checking RT-level benchmarks with thousands of properties efficiently.