Architecture validation for processors

• Main Authors: Ho, Richard C., Yang, C. Han, Horowitz, Mark A., Dill, David L.
• Format: Conference Proceeding
• Language: English
• Subjects: Automatic control; Automatic generation control; Automatic logic units; Automatic testing; Computer systems organization > Architectures > Parallel architectures > Multiple instruction, multiple data; Computer systems organization > Dependable and fault-tolerant systems and networks > Availability; Computer systems organization > Dependable and fault-tolerant systems and networks > Maintainability and maintenance; Computer systems organization > Dependable and fault-tolerant systems and networks > Reliability; Control systems; Error correction; Formal verification; General and reference > Cross-computing tools and techniques > Reliability; Hardware > Hardware test > Design for testability > Online test and diagnostics; Hardware > Hardware test > Memory test and repair; Hardware > Integrated circuits > Interconnect; Hardware > Integrated circuits > Semiconductor memory; Hardware design languages; Logic testing; Microprocessors
• ISSN: 1063-6897; 0163-5964; 2575-713X
• DOI: 10.1145/223982.224450

Modem, high performance microprocessors are extremely complex machines which require substantial validation effort to ensure functional correctness prior to tapeout. Generating the corner cases to test these designs is a mostly manual process, where completion is hard to judge. Experience shows that the errors that are caught late in the design, many post-silicon, are interactions between different components in very improbable corner case situations. In this paper we present a technique that targets such error-causing interactions by automatically generat- ing test vectors that will cause the processor to exercise all transitions of the control logic in simulation. We use techniques from formal verification to derive transition tours of a fully enumerated state graph of the control logic of the processor. Our system works from a Verilog description of the original machine and is currently being used to validate an embedded dual-issue processor in the node controller of the Stanford FLASH Multiprocessor. Modeling the processor control results in 200K states and an 8M instruction trace to check all transitions of control arcs.