About:

Bug UnderGround is a suite of Verilog designs of fairly complex microprocessors with functional bugs. The majority of the bugs occur in complex corner cases of microprocessor operation and are inspired by publicly available errata from Intel, AMD, and other processor manufacturers.

Disclaimer: the authors do not warrant or assume any legal liability or responsibility for the accuracy, completeness, or usefulness of this software, nor for any damage derived by its use.

Project Members:

• Valeria Bertacco
• Todd Austin
• Ilya Wagner

DLX processor:

DLX is a 5 stage in-order pipeline that runs MIPS-Lite ISA and resolves branches in the ID stage.

• Readme file with bug descriptions
• Buggy Verilog designs: targ.gz [370KB]
• Correct Verilog designs: tar.gz [10K]

In-order Alpha processor:

Alpha is a 5 stage in-order pipeline that runs a subset of Alpha ISA, with branches resolved in the EX stage and has two-cycle stores.

• Readme file with bug descriptions
• Buggy Verilog designs: targ.gz [133KB]
• Correct Verilog designs: tar.gz [14KB]

Publications:

StressTest

StressTest is a directed-random test generator for hardware verification. It consists of a Markov-model random instruction generator and activity monitors. The model is generated from the user specified template programs and is used to generate the instructions sent to the design under test (DUT). In addition, the user specifies key activity points within the design that should be stressed and monitored throughout the simulation. The StressTest engine then uses closed-loop feedback techniques to transform the Markov model into one that effectively stresses the points of interest. In parallel, StressTest monitors the correctness of the DUT response to the supplied stimuli, and if the design behaves unexpectedly, a bug and a trace that leads to it are reported.

• pdf [585KB]
• ppt [500KB]

Field-Repairable Control Logic

Correctness is a paramount attribute of any microprocessor design; however, without novel technologies to tame the increasing complexity of design verification, the amount of bugs that escape into silicon will only grow in the future. We propose a novel hardware patching mechanism that can detect design errors which escaped the verification process, and can correct them directly in the field. We accomplish this goal through a simple field-programmable state matcher, which can identify erroneous configurations in the processor's control state and switch the processor into formally-verified degraded performance mode, once a "match" occurs. When the instructions exposing the design flaw are committed, the processor is switched back to normal mode. We show that our approach can detect and correct infrequently-occurring errors with almost no performance impact and has approximately 2% area overhead.

• pdf [427KB]
• ppt [1.42MB]

Semantic Guardians

The ability to guarantee the functional correctness of digital integrated circuits and, in particular, complex microprocessors, is a key task in the production of secure and trusted systems. Unfortunately, this goal remains today an unfulfilled challenge, as even the most straightforward practical designs are released with latent bugs. Patching techniques can repair some of these escaped bugs, however, they often incur a performance overhead, and most importantly, they can only be deployed after an escaped bug has been exposed at the customer site. We present a novel approach to guaranteeing correct system operation by deploying a semantic guardian component. The semantic guardian is an additional control logic block which is included in the design, and can switch the microprocessor's mode of operation from its normal, high-performance but error-prone mode, to a a secure, formally verified safe mode, guaranteing that the execution will be functionally correct. We explore several frameworks where a selective use of the safe mode can enhance the overall functional correctness of a processor. Additionally, we observe through experimentation that semantic guardians facilitate the trade-off between the design validation effort and the performance and area cost of the final secure product. The experimental results show that the area cost and performance overheads of a semantic guardian can be as small as 3.5% and 5%, respectively.

• pdf [612KB]
• ppt [1.32MB]