Inferno: Streamlining Verification With Inferred Semantics

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.