1. 4

Abstract: “This work reports on the verification of a complex instruction set computer (CISC) processor, named Y86-64, styled after the Intel64 instruction set using the UCLID5 verifier. We developed a methodology in which the control logic is translated into UCLID5 format automatically, and the pipelined processor and the sequential reference version were described with as much modularity as possible. This work provides confidence in the processor designs presented in the Bryant-O’Hallar on textbook on computer systems, and it also provides a case study for the capabilities and performance of UCLID5.”

  1. 2

    These kind of reports always look super interesting to me, but I rarely put in the effort to study them closely. One reason for this is that the verification language always seems a bit obscure to me. For now I printed the first half of the report. I will print and read the rest if it seems interesting.

    Sidenote: I wonder if CISC processors are significantly harder to verify than RISC processors. Surely x86-64 must be a bitch to verify just due to the sheer number of instructions. For more reasonably sized instruction sets, I would expect that, once you’ve set up the formal descriptions for the different modules, verifying additional instructions is relatively fast.

    1. 2

      I think the complexity of the algorithms, custom logics, and interactions make the difficulty go up for x86. Jared Davis used ACL2 at Centaur to do verification of their x86 processors. There have been a few processors designed for verification. VAMP and AAMP7G come to mind. The former was DLX-style, RISC processor. The latter involved microcode, too. The methodology used on AAMP7G was also used on software. Although mainly used for concurrency and protocols, some also model-check hardware in SPIN to find bugs more easily. Abstract, State Machines are also a flexible method with tool support that’s getting more popular for combined hardware/software verifications.

      Use of Formal Verification at Centaur Technology

      Formal Verification of VAMP Processor

      A Robust, Machine-Code, Proof Framework for Highly-Secure Applications

      Simple Example of Hardware Verification with SPIN