Understanding designers' intentions and accurately verifying a design are major obstacles for verification engineers today. Currently available debugging tools, such as waveform viewers, are unwieldy, often requiring the user to search through millions of cycles of logic simulation data to locate a problem. In this paper, we present Inferno, a novel solution capable of automatically extracting semantic information from a design's interface from simulation information. The semantic structure of an interface's communication protocol is presented to the user as a set of transactions, that is, monolithic communication units that have typically been observed several times during the logic simulation. Transactions can graphically be presented to the user and used as an aid to understand and validate the communication protocol of a design's interface. In addition, approved transactions can also be encoded as assertions expressed in a hardware description language (HDL) and used in constrained-random simulation to certify that the interface protocol adheres to the set of observed (and user-approved) transactions. Moreover, we developed a new closed-loop verification methodology based on Inferno, called transactional verification, which leverages approved transactions to describe correct design behavior. In our methodology, transactions are concurrently extracted during a constraint-based random simulation: the anomalous ones are flagged as potentially buggy and presented to the user for inspection. In the experimental results, we evaluate the performance and the quality of the results of Inferno on a broad range of testbench designs and several of their interfaces, including a number of communication intellectual properties and the OpenSPARC T1 8-core processor from Sun.

The widening gap between CPU complexity and verification capability is becoming increasingly more salient. It is impossible to completely verify the functionality of a modern microprocessor before shipping, much less before tape out. Recent studies indicate that the majority of errors in these designs are centered on control and forwarding logic. To address this problem, we present Chico, an efficient approach to on-chip hardware correctness that specifically targets escaped design errors in these high risk functional blocks. Our solution includes an on-chip checker block that monitors the correctness of potential data dependencies and program order of the executed instructions before they are allowed to commit. If this online checker detects a mismatch, the processor's exception handler is invoked, reconfiguring the system to a known-correct, formally-verified mode of operation which can correctly re-execute and commit the faulty instruction. The processor can then resume its normal, high throughput mode of operation. In our experimental setup, we have implemented Chico in an out-of-order processor design and evaluated its performance impact on 11 distinct buggy variants of the design running SPECint benchmarks. Our results indicate that Chico can overcome the errors present in these buggy designs at a minimal performance cost, ranging from less than 1% up to 4%. In addition, we evaluated Chico's area cost and found it to be an order of magnitude smaller than other popular solutions such as DIVA, with an area impact of less than 3% for our experimental processor. Our approach is novel in that it shows no appreciable performance degradation on a correct design, and it is a low complexity, area-frugal solution compared to previous work.

Modern processor designs are extremely complex and difficult to validate during development, causing a growing portion of the verification effort to shift to post-silicon, after the first few hardware prototypes become available. Extremely slow simulation speeds during pre-silicon verification result in functional errors escaping into silicon, a problem that is further exacerbated by the growing complexity of the memory subsystem in multi-core platforms. In this work we present CoSMa, a novel technology offering high coverage functional post-silicon validation of cache coherence protocols in multicore systems. It enables the detection and diagnosis of functional errors in the memory subsystem by recording at runtime a compact encoding of the operations occurring at each cache line and checking their correctness at regular intervals. We leverage the system's existing memory resources to store the required activity, thus minimizing area overhead. When the system is finally ready for customer shipment, CoSMa can be completely disabled, eliminating any performance or memory overhead. We reproduce in our experiments a set of coherence protocol bugs based on published errata documents of commercial multicore designs, and show that CoSMa is highly effective in detecting them.