In this paper we outline a theory for the environment-modeling problem , the problem of abstracting component finite state machines (FSMs)bordering a particular FSM of interest within a network of interacting FSMs. The goal is to lay a theoretical foundation for the automatic state reduction of large FSM networks. We feel this is a prerequisite for the efficient use of many verification techniques. We focus on computing conditions for the safe removal of a component FSM in a FSM network, where removal is safe if it preserves a certain well-defined trace equivalence. We present an optimized algorithm for determining language universality of a FSM, as well as determining independence of a FSM from those of its inputs connected to outputs of neighboring FSMs. These two properties, input independence and language universality, provide the necessary and sufficient conditions for safe removal. In addition, we show how simulation relations can be utilized, both to reduce the cost of computing safe removal and to create an appropriate abstract FSM when safe removal is not possible.

We present a new algorithm for detecting both combinationally and sequentially false timing paths, one in which the constraints on a timing path are captured by justifying symbolic functions across latch boundaries.We have implemented the algorithm and we present, here, the results of using it to detect false timing paths on a recent PowerPC microprocessor design.We believe these are the first published results showing the extent of the false path problem in industry.Our results suggest that the reporting of false paths may be compromising the effectiveness of static timing analysis.

In this paper we report on new techniques for verifying contentaddressable memories (CAMs), and demonstrate that these techniqueswork well for large industrial designs. It was shown in [Formal verification of PowerPC(TM) arrays using symbolic trajectory evaluation], that theformal verification technique of symbolic trajectory evaluation (STE)could be used successfully on memory arrays. We have extended thatwork to verify what are perhaps the most combinatorially difficultclass of memory arrays, CAMs. We use new Boolean encodings toverify CAMs, and show that these techniques scale well, in that spacerequirements increase linearly, or sub-linearly, with the various CAMsize parameters.In this paper, we describe the verification of two CAMs froma recentPowerPC microprocessor design, a Block Address Translation unit(BAT), and a Branch Target Address Cache unit (BTAC). The BATis a complex CAM, with variable length bit masks. The BTAC is a64-entry, 64-bits per entry, fully associative CAM and is part of thespeculative instruction fetch mechanism of the microprocessor. Webelieve that ours is the first work on formally verifying CAMs, and webelieve our techniques make it feasible to efficiently verify the varietyof CAMs found on modern processors.

When silicon is available, newly designed microprocessors ore tested in specially equipped hardware laboratories, where real applications can be run at hardware speeds. However, the large volumes of code being run, plus the limited access to the internal nodes of the chip, make it extraordinarily difficult to characterize the nature of any failures that occur. In this paper, we describe how the formal verification technique of temporal logic model checking was used to quickly characterize a design error exhibited during hardware testing of the PowerPC 620 microprocessor. We claim that model checking can efficiently characterize such failures when certain pre-conditions are met. We also show how the same error could have been revealed early in the design cycle, by model checking a short and simple correctness specification. We discuss the implications of this for verification methodologies over the full design cycle.

Verifying memory arrays such as on-chip caches and register files is a difficult part of designing a microprocessor.Current tools cannot verify the equivalence of the arrays to their behavioral or RTL models, nor their correct functioning at the transistor level.It is infeasible to run the number of simulation cycles required, and most formal verification tools break down due to the enormous number of state-holding elements in the arrays.The formal method of symbolic trajectory evaluation (STE) appears to offer a solution, however.STE verifies that a circuit satisfies a formula in a carefully restricted temporal logic.For arrays, it requires only a number of variables approximately logarithmic in the number of memory locations.The circuit is modeled at the switch level, so the verification is done on the actual design.We have used STE to verify two arrays from PowerPC microprocessors: a register file, and a data cache tag unit.The tag unit contains over 12,000 latches.We believe it is the largest circuit to have been formally verified, without abstracting away significant detail, in the industry.We also describe an automated technique for identifying state-holding elements in the arrays, a technique which should greatly assist the widespread application of STE.