Model checking for a first-order temporal logic using multiway decision graphs

Using Ordered Binary Decision Diagrams (OBDD) to encode sets of states, the transition relations, and to perform an implicit enumeration of the state space, symbolic model checking has proven to be a very practical technique for the automatic verification of hardware designs at the propositional logic level. However, these methods still require the description of the design to be at the Boolean logic level, and thus in general they are not adequate for verifying circuits with large datapath again because of the state explosion problem. That is, the number of states in the model grows exponentially with the number of state variables and therefore, even with OBDD encoding the data structures become too large to fit typical current computer memories.; In this thesis, we study the automatic model checking with a first-order branching time temporal logic. Compared to other researches, we raise the of state machines (ASMs). An ASM is encoded using Multiway Decision Graphs (MDGs), of which Reduced Ordered Binary Decision Diagrams (ROBDDs) are a special case. ASMs can be used to describe designs at Register Transfer Level (RTL). The verification of ASMs is based on state enumeration whose complexity is independent of the width of the datapath.; The main task of the thesis is to define a first-order branching time temporal logic called Abstract-CTL* and develop property checking algorithms for a subset of Abstract-CTL* called L_MDG, which includes safety properties and liveness properties with or without fairness constraints. The main property templates in L_MDG include A_p, AG_p, AF _p, A_p U_q, AG( c =>(F p)) and AG(c => pU q), where c, p and q are Next_let_formulas which contain only the temporal operator X (“Next”), G, F, U means “always”, “eventually”, “until” respectively, and A means “for all computation paths”. In general, our approach to model checking is to automatically build additional ASMs that represent the Next_let_formulas appearing in a property, connect these additional ASMs to the original one to be verified, and then check a simpler property on the composite machine.