We present a framework for validating the compliance of a design with a given architecture. Our approach is centered on the concept of misinterpretations. These include missing behavior, wrong understanding of a behav...
详细信息
ISBN:
(纸本)9781595937711
We present a framework for validating the compliance of a design with a given architecture. Our approach is centered on the concept of misinterpretations. These include missing behavior, wrong understanding of a behavior, or confusion with similar behavior described in the architecture or elsewhere. We formally capture the architecture behavior in the form of flowcharts and automatically derive a list of architecture misinterpretations from these flowcharts. These misinterpretations constitute the backbone of coverage models targeted by a suite of tests. The suite is automatically generated by a model-based test case generator. A compliance validation System based on these principles has been developed and used in two actual industrial processes of checking compliance with the PowerPC architecture.
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 gro...
详细信息
ISBN:
(纸本)1595933816
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. In this paper, 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.
The logic of Equality with Uninterpreted Functions (EUF) provides a means of abstracting the manipulation of data by a processor when verifying the correctness of its control logic. By reducing formulas in this logic ...
详细信息
The logic of Equality with Uninterpreted Functions (EUF) provides a means of abstracting the manipulation of data by a processor when verifying the correctness of its control logic. By reducing formulas in this logic to propositional formulas, we can apply Boolean methods such as ordered Binary Decision Diagrams (BDDs) and Boolean satisfiability checkers to perform the verification. We can exploit characteristics of the formulas describing the verification conditions to greatly simplify the propositional formulas generated. We identify a class of terms we call “p-terms” for which equality comparisons can only be used in monotonically positive formulas. By applying suitable abstractions to the hardware model, we can express the functionality of data values and instruction addresses flowing through an instruction pipeline with p-terms. A decision procedure can exploit the restricted uses of p-terms by considering only “maximally diverse” interpretations of the associated function symbols, where every function application yields a different value except when constrained by functional *** present two methods to translate formulas in EUF into propositional logic. The first interprets the formula over a domain of fixed-length bit vectors and uses vectors of propositional variables to encode domain variables. The second generates formulas encoding the conditions under which pairs of terms have equal valuations, introducing propositional variables to encode the equality relations between pairs of terms. Both of these approaches can exploit maximal diversity to greatly reduce the number of propositional variables that need to be introduced and to reduce the overall formula *** present experimental results demonstrating the efficiency of this approach when verifying pipelined processors using the method proposed by Burch and Dill. Exploiting positive equality allows us to overcome the exponential blow-up experienced previously when verifying microprocessors wi
This paper addresses the problem of formally verifying the correctness of a complex pipelined microprocessor at the micro-architectural level of abstraction. The design verified is an example out-of-order execution pr...
详细信息
This paper addresses the problem of formally verifying the correctness of a complex pipelined microprocessor at the micro-architectural level of abstraction. The design verified is an example out-of-order execution processor with a reorder buffer, a store buffer, branch prediction, speculative execution and exceptions. We propose a systematic approach called the Completion Functions Approach to decompose and incrementally build its proof of correctness. The central idea is to construct the abstraction function using completion functions, one per unfinished instruction, each of which specifies the effect on the programmer visible state components of completing the instruction. This construction of the abstraction function leads to a very natural decomposition of the proof into proving a series of verification conditions. The approach prescribes a systematic way to generate these verification conditions which can then be discharged with a high degree of automation using techniques based on decision procedures and rewriting. The verification was completed in 34 person days, which we believe, is a modest investment in return for the significant benefits of formal verification.
This paper presents a technique for formal verification of processors. The verification process is performed at the RTL level of implementation, which has the advantage of being synthesizable by a synthesis tool. Cade...
详细信息
ISBN:
(纸本)0780376579
This paper presents a technique for formal verification of processors. The verification process is performed at the RTL level of implementation, which has the advantage of being synthesizable by a synthesis tool. Cadence SMV is used as the verification tool. It employs the symbolic model checking technique. A stepwise verification method is proposed where the details of design are increased in each step. This method facilitates the error finding process. The proposed technique can reduce the complexity of the verification process and enables it to be completed in a reasonable time. The technique is illustrated on a simple processor used in an embedded web server. The design is verified successfully.
The phrase model checking refers to algorithms for exploring the state space of a transition system to determine if it obeys a specification of its intended behavior. These algorithms can perform exhaustive verificati...
详细信息
The phrase model checking refers to algorithms for exploring the state space of a transition system to determine if it obeys a specification of its intended behavior. These algorithms can perform exhaustive verification in a highly automatic manner, and, thus, have attracted much interest in industry. Model checking programs are now being commercially marketed. However, model checking has been held back by the state explosion problem, which is the problem that the number of states in a system grows exponentially in the number of system components. Much research has been devoted to ameliorating this problem. In this tutorial, we first give a brief overview of the history of model checking to date, and then focus on recent techniques that combine model checking with satisfiability solving. These techniques, known as bounded model checking, do a very fast exploration of the state space, and for some types of problems seem to offer large performance improvements over previous approaches. We review experiments with bounded model checking on both public domain and industrial designs, and propose a methodology for applying the technique in industry for invariance checking. We then summarize the pros and cons of this new technology and discuss future research efforts to extend its capabilities.
In this paper a practical methodology for formally verifying RISC cores is presented. Using a hierarchical model which reflects the abstraction levels used by designers of real RISC processors, proofs between neighbor...
详细信息
In this paper a practical methodology for formally verifying RISC cores is presented. Using a hierarchical model which reflects the abstraction levels used by designers of real RISC processors, proofs between neighboring levels are performed for simplifying the verification process. The proofs are performed by showing that each instruction is executed correctly by the pipelined machine with respect to the semantics of the instruction set architecture. During this proof, temporal abstractions are used to find correspondences between the various levels of abstractions. Additionally, lower level implementational details such as, multiphased clocks and gate level descriptions of the final implementation, are accounted for. The overall correctness proof is managed in two complementary steps, namely, pipeline data and pipeline control correctness. In the former, we show that the cumulative effect of pipeline suboperations yields the data semantics of architecture instructions. While in the latter, we are concerned with interferences (conflicts) between the different instructions and suboperations in the pipeline. We have developed a set of parametrized proof scripts which highly automate the different proof tasks. In addition, the pipeline control proof is constructive, in the sense that the conditions under which the pipeline conflicts occur are automatically generated and explicitly stated thus aiding the user in its removal. All developed specifications and proof scripts are kept general, so that the methodology could be applied for a wide range of RISC cores (e.g., those used in embedded systems). In this paper, the described formalization and proof strategies are illustrated via the DLX RISC processor.
暂无评论