Abstract

As the complexity of hardware digital systems increases, their correctness becomes a major concern. Traditional verification by simulation is infeasible to exhaustively test and guarantee correctness. More than a decade ago, however, formal verification has been introduced as complement technique to simulation. Formal methods establish that a design implementation satisfies its specification by mathematical reasoning. Among several techniques, model checking is one of the most successful technology, which is based on the exploration of the design state space. In this thesis, we propose a new model checking method based on the theory of }-automata and multiway decision graphs (MDGs). Unlike reduced ordered binary decision diagrams (ROBDDs), MDGs allow system models to be described using abstract state machines (ASMs) through abstract data sorts and uninterpreted function symbols, hence enabling the verification of larger designs independent of the datapath width. Given an ASM and a first-order linear time temporal logic property, the model checking problem proposed in this thesis is reduced to a language emptiness checking of an }-automaton that accepts all }-words produced by the system violating the property formula. The checking method comprises four steps: (1) transforming the first-order property into a propositional formula by constructing ASMs for the atomic formulas of the property; (2) generating an }-automaton from the negation of the transformed propositional formula; (3) computing the product of the generated automaton, the system model ASM and the constructed ASMs; and (4) applying a language emptiness checking algorithm on the product automaton. Three different checking algorithms have been developed, implemented, and proved correct in this thesis. To evaluate the performance of the proposed model checking method and implemented tool, we conducted several experimentations and case studies. We also compared the efficiency of our tool with an existing MDG regular model checking application, as well as with popular ROBDD-based automata model checking tools such as VIS. Our model checker was found to be outperforming the above tools.