Hybrid methods for satisfiability checking in register-transfer level circuits
Kwang-Ting Tim Cheng, G. Parthasarathy · 2005
Designers of electronic hardware systems face dual challenges of increasing system complexity and decreasing time for design implementation. It is desirable that designers can implement, verify, and test their designs in as high a level of abstraction as possible. Consequently, computer-aided design methods that can take advantage of these abstract representations to enhance performance have become necessary. One of the fundamental problems in designing such methods is that of checking whether a propositional formula evaluates a desired value or proving that no such value exists or the satisfiability problem. In this work, we focus on circuits modeled at the register-transfer level (RTL), where operations on data values are modeled as operations on collections of bits or as integers. RTL descriptions consist of interacting FSMs which are mostly Boolean operations on bits and latches; and arithmetic operations on bit-vectors and registers. The former is called the control and the latter is called the data-Path. We approach the problem by first proposing a SAT based approach to search in the sequential space of the Boolean control. The method uses cube-based abstraction to perform implicit backward enumeration of reachable states. We analyze the performance of this method versus methods like Binary Decision Diagrams and Bounded Model Checking. We next propose a method to perform combined branch-and-bound search in the Boolean and integer domains by using interval arithmetic as a pessimistic abstraction for constraint propagation in the data-path. We describe how RTL can be translated to arithmetic and Boolean constraints and efficiently solved. We also propose data-structures and algorithms for efficient constraint propagation, and search bounding. We then propose static learning techniques based on constraint propagation, and recursive learning. We describe techniques to guide the decision strategy of the solver based on these methods. Finally, we describe a simplification procedure that allows us to significantly reduce problem size and run-times for RTL satisfiability. We analyze and demonstrate experimentally how each of the proposed techniques adds to overall performance when contrasted with current comparable techniques.