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 inter-nally developed verification tools. If we look more closely, however, we see that the major industrial applications of formal verification have been either in verifying individ-ual 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. Attempt-ing 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 operatio