Bryant, Randal E. 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. Most existing verifiers model system operation at a detailed bit level. We have developed UCLID, a prototype verifier for infinite-state systems. The UCLID modeling language extends that of SMV, a bit-level model checker, to include integer and function state variables, addition by constants, and relational operations. The underlying logic is expressive enough to model a wide range of systems, but it still permits a decision procedure where we transform the formula into propositional logic and then use either binary decision diagrams (BDD) or a Boolean satisfiability (SAT) solver. computer sciences 1988-01-01
    https://kilthub.cmu.edu/articles/journal_contribution/System_Modeling_and_Verification_with_UCLID/6610211
10.1184/R1/6610211.v1