We present an approach to modeling and verifying machine-code programs that exhibit non-determinism. Specifically, we add support for system calls to our formal, executable model of the user-level x86 instruction-set architecture (ISA). The resulting model, implemented in the ACL2 theorem-proving system, allows both formal analysis and efficient simulation of x86 machine-code programs; the logical mode characterizes an external environment to support reasoning about programs that interact with an operating system, and the execution mode directly queries the underlying operating system to support simulation. The execution mode of our x86 model is validated against both its logical mode and the real machine, providing test-based assurance that our model faithfully represents the semantics of an actual x86 processor. Our framework is the first that enables mechanical proofs of functional correctness of user-level x86 machine-code programs that make system calls. We demonstrate the capabilities of our model with the mechanical verification of a machine-code program, produced by the GCC compiler, that computes the number of characters, lines, and words in an input stream. Such reasoning is facilitated by our libraries of ACL2 lemmas that allow automated proofs of a program's memory-related properties.

SUMMARY Several proof formats have been used to verify refutations produced by satisfiability (SAT) solvers. Existing formats are either costly to check or hard to implement. This paper presents a practical approach that facilitates checking of unsatisfiability results in a time similar to proof discovery by embedding clause deletion information into clausal proofs. By exploiting this information, the proof‐checking time is reduced by an order of magnitude on medium‐to‐hard benchmarks as compared to checking proofs using similar clausal formats. Proofs in a new format can be produced by making only minor changes to existing conflict‐driven clause‐learning solvers and their preprocessors, and the runtime overhead is negligible. This approach can easily be integrated into Glucose 2.1, the SAT 2012 challenge winner, and SatELite, a popular SAT‐problem preprocessor. Copyright © 2014 John Wiley & Sons, Ltd.

In recent years, leading microprocessor companies have made huge investments to improve the reliability of their products. Besides expanding their validation and CAD tools teams, they have incorporated formal verification methods into their design flows. Formal verification (FV) engineers require extensive training, and FV tools from CAD vendors are expensive. At first glance, it may seem that FV teams are not affordable by smaller companies. We have not found this to be true. This paper describes the formal verification framework we have built on top of publicly-available tools. This framework gives us the flexibility to work on myriad different problems that occur in microprocessor design.

We present a framework for post-silicon analysis, that provides a formal, bidirectional communication with pre-silicon verification. We show how to exploit the framework to provide a formal guarantee on post-silicon verification accuracy under limited observability. In particular, we partition a pre-silicon assertion checker (with full observability) into (1) a limited-observability checker and (2) an in-silicon integrity unit. The composition of the two units is guaranteed to provide the same accuracy as a pre-silicon checker. We apply the framework in the verification of a cache system.

We present a method for verifying information flow properties of software programs using inductive assertions and theorem proving. Given a program annotated with information flow assertions at cutpoints, the method uses a theorem prover and operational semantics to generate and discharge verification conditions. This obviates the need to develop a verification condition generator (VCG) or a customized logic for information flow properties. The method is compositional: a subroutine needs to be analyzed once, rather than at each call site. The method is being mechanized in the ACL2 theorem prover, and we discuss initial results demonstrating its applicability.

We propose instruction-driven slicing, a technique for annotating microprocessor descriptions at the register transfer level (RTL) in order to achieve lower power dissipation. Our technique automatically annotates existing RTL code to optimize the circuit for lowering power dissipated by switching activity. Our technique can be applied at the architectural level as well, achieving similar power gains. We demonstrate our technique on architectural and RTL models of a 32-bit OpenRISC processor (OR1200), showing power gains for the SPEC2000 benchmarks

A link between the ACL2 and HOL4 proof assistants is described. This allows each system to be deployed smoothly within a single formal development. Several applications are being considered: using ACL2's execution environment for simulating HOL models; using ACL2's proof automation to discharge HOL proof obligations; and using HOL to specify and verify properties of ACL2 functions that cannot easily be stated in the first-order ACL2 logic. Care has been taken to ensure sound translations between the logics supported by HOL and ACL2. The initial ACL2 theory has been defined inside HOL, so that it is possible to prove mechanically that first-order ACL2 functions on S-expressions correspond to higher-order functions operating on a variety of types. The translation between the two systems operates at the level of S-expressions and is intended to handle large hardware and software models

We describe our formal specification of Motorola's Complex Arithmetic Processor (CAP) DSP and our subsequent use of this specification to verify the correctness of several DSP algorithms. We wrote the specification in the ACL2 logic and carried out the mechanical proofs using the ACL2 theorem-proving system. Motorola's CAP is a super-scalar, pipelined DSP with seven memories and more than 20 functional units. Our formal specification is bit-for-bit exact, and was created by hand translating Motorola's drawings for the CAP. We believe that the specification developed is the largest of its kind, as this is the only formal specification of which we are aware for a complete commercial design. Proving the correctness of the DSP algorithms (programs) required proving the correctness of programs with 317-bit instructions and a non-interlocking execution pipeline. This Motorola DSP has a 1.8 million transistor implementation. This project involved both CLI and Motorola personnel and represents more than eight man-years of effort.

Current verification technology provides tools for the verification of programs written in a high-level language. Even verified high-level programs may not satisfy their specifications when executed, due to errors in tower-level software and hardware. We discuss an attempt at eliminating this problem with the design of an execution environment consisting of a compiler, operating system, and processor, each of which has been mechanically verified.