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.

Test generation for datapath floating-point verification involves targeting intricate corner cases, which can often be solved only through complex constraint solving. In the process of calculating the result, we use an intermediate result whose significand comprises a finite number of bits and a sticky bit that is 0 if and only if the intermediate result is exact. We refer to all the bits beyond those represented in the final result as the invisible bits. We deal with corner cases that can only be defined via constraints on the intermediate result. Our work investigates the following problem: given a floating-point operation, and constraints on the invisible bits and the sticky bit, find two inputs for the operation that yield an intermediate result compatible with the constraints. The paper supplies a deterministic solution for addition and subtraction, and probabilistic solutions for multiplication and division. It also discusses the application of these algorithms to the verification of floating-point implementations.

Coverage analysis is used to monitor the quality of the verification process. Reports provided by coverage tools help users identify areas in the design that have not been adequately tested. Because of their sheer size, the analysis of large coverage models can be an intimidating and time-consuming task. Practically, it can only be done by focusing on specific parts of the model. This paper presents a method for defining views onto the coverage data of cross-product functional coverage models. The proposed method allows users to focus on certain aspects of the coverage data to extract relevant, useful information, thereby improving the quality of the coverage analysis. A number of examples are provided that show how the proposed method improved the verification of actual designs.

We present algorithms that solve the following problem: given three ranges of floating-point numbers R/sub x/, R/sub y/, R/sub z/, a floating-point operation (op), and a rounding-mode (round), generate three floating-point numbers x~, y~, z~ such that x~/spl isin/R/sub x/, y~/spl isin/R/sub y/, z~/spl isin/R/sub z/ and z~=round(x~ op y~). This problem, although quite simple when dealing with intervals of real numbers, is much more complex when considering ranges of machine numbers. We provide full solutions for add and subtract, and partial solutions for multiply and divide. We use range constraints on the input operands and on the result operand of floating-point instructions to target corner cases when generating test cases for use in verification of floating-point hardware. The algorithms have been implemented in a floating-point test-generator and are currently being used to verify floating-point units of several processors.