System Modeling and Verification with UCLID

Formal verification has had a significant impact on the semiconductor industry, particularly for companies that can devote significant resources to creating and deploying internally developed verification tools. If we look more closely, however, we see that the major industrial applications of formal verification have been either in verifying individual blocks, such as floating-point units and memories, or in verifying an abstracted representation of some aspect of the system, such as a cache coherence protocol. Attempting to verify overall system correctness is beyond the reach of current tools. For example, these tools are not capable of verifying that an out-of-order execution microprocessor correctly replicates the behavior of its sequential instruction set architecture (ISA) model. Most existing verification tools model system operation at a detailed bit level. Using powerful inference engines, such as Binary Decision Diagrams (BDDs) and Boolean satisfiability (SAT) checkers, symbolic model checkers [3, 5] and similar tools can analyze all possible behaviors of very large, finite-state systems. Modeling a system at the bit level makes it difficult to scale formal verification to systems that store and manipulate large amounts of data, such as microprocessors and many forms of embedded software. The many bits of state held in the various memories, queues, and caches lead to state explosion problems that overwhelm even the most advanced model checkers. Taking a cue from the hardware design principle of separating data from control, we believe that systems should be modeled and verified using a more abstract representation of data. If we assume individual functional units, such as ALUs and instruction decoders can be verified separately, then there is no need to track the value of every bit in the system. Instead, we can represent words of data as symbolic term values that are generated by function units, communicated among different subunits, and stored in different buffers and memories. For some term value x, we need not keep track of its bit width, its encoding, or even its actual value. With this term-level abstraction of data, verification can focus on the behavior of the control logic