Overview

Semiconductor Research Corporation is identified in the available evidence as a funding organization for the 2018 Carnegie Mellon University technical report “Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5” by Randal E. Bryant. The report states that the work was supported, in part, by Semiconductor Research Corporation under contract 2637.001.[1]

Supported technical work

The supported report presents a formal-verification case study for pipelined Y86-64 microprocessors using the UCLID5 verifier. The processor is described as a complex instruction set computer styled after the Intel64 instruction set.[2]

The work developed a methodology in which processor control logic was translated automatically into UCLID5 format, while both the pipelined processor and a sequential reference version were modeled with as much modularity as possible.[2]

Verification objective and result

The report’s stated goals were to check the correctness of Y86-64 pipeline processor designs and to evaluate UCLID5’s capabilities for modeling and verifying hardware designs.[3] The reported result was that the different pipeline processors generate the same results as the sequential reference model for all possible programs.[3]

Evidence scope

Within the provided evidence, Semiconductor Research Corporation is documented only through its partial support of this specific formal-verification report.