Veri cation Through the Principle of Least Astonishment

Assessing the correctness of a digital design is a challenging task hampered by extremely large circuit netlists, counterintuitive property descriptions and ill-defined specifications. In this paper we propose a new verification methodology, inspired by the principle of least astonishment. The underlying idea is to provide an automatic assessment of what constitutes "common behavior" for a system, and use this to detect any anomaly in the design. Deviant behavior is presented to the verification engineer through intuitive, compact diagrams which lend themselves to quick inspection for correctness. To enable this methodology we introduce Inferno, a new tool which can analyze the results of a logic simulation trace and automatically extract high-level diagrams representing the design\´s transaction activity across any user-defined interface. In addition, Inferno can automatically generate a checker module corresponding to a given transaction, suitable for use in a wide range of verification methodologies. We envision the deployment of Inferno in a closed-loop constraint-random simulation methodology where any new transaction detected on the interface is presented to the user for analysis and, once deemed legal, it is merged into an "approved transactions" checker, which flags the detection of any new type of transactions. We provide a series of examples and experimental results to show the effectiveness of Inferno and some of its possible uses