Multiway decision graphs and their applications in automatic formal verification of rtl designs
Xiaoyu Song, E. Cerny, Zijian Zhou · 1997
Formal verification methods have been considered as a powerful complementary approach to simulation in digital system design. This thesis studies the problem of automatically verifying designs having both non-trivial datapath and control circuitry. We propose a new class of decision graphs, called Multiway Decision Graphs (MDGs), as an efficient representation for Register-Transfer level designs, using a many-sorted first-order logic with a distinction of abstract and concrete sorts. In an MDG, a data signal is represented by a single variable of abstract sort rather than by a vector of Boolean variables, and a data operation is represented by an uninterpreted function symbol that could be partially interpreted using rewrite rules when necessary. The verification is carried out at a high level in the design hierarchy with a runtime independent of the width of the datapath. Our approach is well suited for the verification of microprocessors or designs produced from high level synthesis where data operations can be viewed as black boxes. This thesis contains most of the research results on MDGs and MDG-based verification. A state enumeration technique exploiting MDGs is explained for exploring the state space of the abstract descriptions of state machines. Various MDG-based verification techniques are developed, such as verification of combinational circuits, invariants, behavioral equivalence of synchronous circuits, and non-pipelined microprocessors against their instruction set architectures. A term rewriting algorithm makes it possible to partially interpret the uninterpreted function symbols in MDGs. The verification prototype that we implemented includes the above verification applications and establishes a platform for further development of MDG-based techniques. Finally, two case studies are presented: First, an illustrative case study on an Island Tunnel Controller where the non-termination problem of the state enumeration procedure is addressed, and then a case study on a real ATM switch fabric where the effectiveness and applicability of our methods are demonstrated.