Recent dramatic productivity gains in a designer's ability to generate gates have stemmed from the advancements and widespread acceptance of synthesis technology into today's design flowsýin fact, design productivity has risen tenfold since the late 1980s, to over 140 gates per day. Unfortunately, design verification engineers are currently able to verify only the RTL equivalent of approximately 100 gates per day. Moreover, designers must now comprehend the byzantine relationships, dependencies, and interactive complexity associated with a larger set of functional objects, all resulting from the productivity gains of synthesis. Clearly, we should place proportional emphasis on coding RTL to increase our verification productivity, matching our attention to insuring an optimal synthesis process.

The likelihood and cost of design errors generally rise with complexity. Fortunately, design errors detected early in the design process can be corrected far more easily and at a smaller cost than those detected later.

Design errors detected after the product is shipped in large numbers to the marketplace can result in prohibitive costs. Design errors found prior to customer release are expensive as well, leading to long cycles of regression test reruns, an inability to run self-test on first silicon, respins of silicon, and ultimately, delayed time-to-market.

A simple code

These experiences have forced project managers and ASIC design engineers to focus more of their attention on all aspects of design verification. Therefore, the performance of design and analysis tools is of paramount concern within any verifiable RTL methodology. Without doubt, selecting a single RTL coding styleýone that maximizes the performance of simulation, Boolean equivalence, and model-checking, as well as achieving an optimal flow through synthesis and physical designýis a formidable task. To address the problem of competing tool coding requirements, we have developed three essential techniques and methodologies: an object-oriented hardware design (OOHD) methodology, incorporating modern programming language principles; a simplified and tool-efficient verifiable subset of RTL Verilog; and a tool-performance-enhancing and design-error linting strategy targeted as the initial check in a complete line of verification tools.

This RTL verification-centric methodology creates a number of advantages. It permits a seamless optimization of design processes throughout the duration of the design and enables a seamless augmentation of new processes. In addition, it leaves the designer's text and functional intent undisturbed throughout the duration of the design. It also offers cooperation and support for multiple EDA tools while achieving higher verification coverage in minimal time. Finally, it clarifies the design intent at the RT level.

Object-oriented hardware design

Developed in the mid-1960s, the original hardware description languages (HDLs) addressed the deficiencies of building hardware models using first-generation higher-level programming languages. For example, higher-level programming languages during this period lacked support for concurrency and a correspondence or relationship to a specific hardware implementation, at least in modeling at the RT level. Such features are critical for hardware design analysis and synthesis automation. Today Verilog and VHDL have evolved to support the concepts and advancements in modern programming languages as well as the principles that underlie good programming practices. The decision to apply these programming principles when coding in HDLs, however, generally remains up to the engineer.

In 1972, Professor D. L. Parnus of Carnegie Mellon University introduced the programming principle of information hiding, which instructs designers to hide details pertaining to a single design decision (particularly a design decision that is likely to change) within a program module. The principle enables designers to isolate or localize the design decision details within a module, allowing their interface relationship with other segments of the design to create a level of design abstraction (a phenomenon known as the abstraction principle).

Figure 1 - Object Orientation

The object-oriented hardware design flow allows a higher level of abstraction, speeding the design and verification processes.

Engineers are accustomed to creating multiple levels of abstraction within the design's RTL description by partitioning and localizing related functionality into a module description. To optimize each EDA tool's performance, we recommend that information hiding be applied (at a minimum) to each distinct grouping of state elements within the design's RTL. This technique allows each register bit (the fundamental building block of a RTL specification) to be functionally grouped into a single object and detailed at a lower level of abstraction. Our project CAD group can automatically generate tool-specific libraries, which provide the lower level of abstraction details in an optimized EDA process format. The object's abstraction interface within the RTL specification permits the referencing of a targeted tool-specific optimized library for each process point within the design flow. Equivalence checking validates the functional consistency between the targeted libraries (see Figure 1).

By applying information hiding to the "functional grouping" of state elements within the RTL, and introducing a new level of design abstraction, we have succeeded in isolating design details within tool-specific libraries. This methodology allows us to simultaneously optimize the performance of simulation, equivalence-checking, model-checking, and physical design within our ASIC design flow. Furthermore, our methodology allows us to add new features and tools throughout the course of a project, without interfering with the text or functional intent of the original design. For example, during our last project we added a new mechanism for consistent random initialization of all registers, which was encapsulated within the simulation-targeted library. Without our OOHD methodology, thousands of lines of code, involving hundreds of files, would require modification to support this new verification feature within our ASIC designs.

Simulation performance

Frequently, to secure the timing performance of logic synthesis, design engineers need to specify explicit vendor macro cell instances within the RTL module specification. To prevent the loss of the designer's functional intent, and to prevent the RTL code from degenerating into a slower-simulating gate-level netlist, we have adapted an RTL coding style (see Listing 1).

Figure 2 - Equivalent Checks

The equivalence checker verification flow eliminates the dreaded gate-level regression simulation while easing the verification process.

We define the implementation text macro during the synthesis process and undefine it during simulation. This combination preserves clarity in the RTL specification and optimizes the RTL for simulation performance, while insuring a specific implementation during synthesis. At this point, we use equivalence checking to verify consistency between the RTL behavior specification and the macro cell instance implementationýsimply a self-compare on the RTL module. Similarly, during the equivalence checker's compilation process, we define the implementation text macro for the implementation model, and undefine it for the specification model.

Equivalence checking

Our equivalence checker verification flow has eliminated the need for lengthy gate-level regression simulation, while increasing verification coverage (see Figure 2). Since 1993, this methodology has enabled our lab to eliminate gate simulation entirely (that is, all verification has remained at the RTL level). Two key elements unique to our verification flow are the final full chip hierarchical-RTL-to-flat-gate equivalence check, followed by simulation of the gate-generated ATPG vectors on the RTL golden model. These steps effectively close the verification loop by identifying any revision-control or process-flow errors, as well as a final functional validation on all libraries used by synthesis, place and route, and ATPG. Equivalence checking at various sequential points within the design flow might otherwise miss these errors. Furthermore, simulating the ATPG vectors on the RTL golden model validates the synthesis tool (and the equivalence checker) by identifying most stylistic or interpretive differences in RTL coding between the simulator and the synthesis tool.

We have observed that adapting an OOHD provides an optimization advantage for automatically identifying all register and latch pairs between the RTL specification and its gate-level implementation. By referencing the equivalence-checking or synthesis-targeted library, we can directly map the hierarchical RTL instances to their synthesized netlist instances (see Figure 3). An equivalence checker efficiently validates the equivalence-checking targeted library against the higher-level simulation-targeted library.

Another equivalence checking optimization advantage the OOHD methodology provides is an automated mechanism for mapping a two-state master-slave latch pair to a single state-point representation (within the RTL specification). The method references a targeted library, optimized for equivalence checking, for all state-element objects in the RTL. The equivalence-checking targeted library is constructed to accurately model the master-slave functionality for each bit, within the functional grouping of state elements instantiated in the RTL. (For instance, a 16-bit instantiated register can be optimally modeled for equivalence checking using 16 lower-level master-slave latch pairs.) Without utilizing a library targeted for equivalence checking, the equivalence checker must invoke more costly routines to identify the two-to-one state mapping between the implementation and the specification.

Figure 3 - From hierarchy to flat

This method references the synthesis targeted library from the RTL during the equivalence-checking process.

Tracking of the number of equivalence checks performed on five different ASICs within our design lab over a 12-month period shows substantial activity (see the table). The "total equivalence checks" column represents all partial and complete design equivalence checks. The "full chip equivalence checks" column represents the verification for the full-chip hierarchical-RTL to flat gate-level netlist comparison. Clearly, the optimizations have allowed all five chips to be thoroughly exercised.

To achieve a high number of equivalence checks as shown in the table requires designers to meet several conditions. The equivalence-checking tool must rest in the hands of the ASIC design engineers (as opposed to the design verification group exclusively). The equivalence-checking tool must be accessible from the desktop. The equivalence-checking tool must run fastýin minutes rather than hours or days. Finally, the design flow must include built-in regression checks (automated in a batch mode, for example).

Code braking

As C. A. R. Hoare pointed out in his 1980 Turing Award Lecture, "There are two ways of constructing a design: one way is to make it so simple that there are obviously no deficiencies, and the other way is to make it so complicated that there are no obvious deficiencies." The choice is obviously clear.

EDA tool vendors generally pride themselves on their support of the entire semantic range of the various HDLs. This support works to the purpose of a large number of customers. But all that coverage creates one serious problem: design teams possess too many alternative methods for expressing the same functionality. Using multiple methods of expression within and across chip designs adds to the overall complexity and, therefore, the cost of verification (in terms of tools, processes, and people resources alike).

With the advent of synthesis technology, a synthesizable RTL subset has emerged, along with checkers for adherence to a vendor-specific synthesis subset. By constraining the rich HDL to a subset of keywords and an explicit coding style, we can use the precise semantics to provide an efficient and clear mapping to a specific hardware implementation.

Other processes within the design flow also benefit from a constrained subset of the full HDL. For example, event-driven simulation provides support for the full range of an HDL. A faster cycle-based simulation model, however, requires an HDL constrained to a precise subset. The cycle-based simulation HDL subset is generally similar from vendor to vendor and similar to the synthesis subset.

Within our design lab we have adopted a simple HDL style that serves all verification tools accepting RTL as well as providing a device for communicating clear functional intent between designers. This simplified RTL Verilog subset can be measured according to the metrics of keywords and operators.

Our verifiable subset emphasizes coding simplicity by using only 28 out of the 102 Verilog reserved words.

Typically, minor changes occur between projects, depending on project-specific needs. We believe that it's important, however, to prevent the RTL description from migrating towards lower- or gate-level keywords. If it's necessary to describe physical or implementation level characteristics, then we've found that the exceptions should be localized and isolated within their own modules. Physical and implementation details shouldn't be embedded directly with the standard RTL used to describe the functional behavior.

On rare exceptions, a few of the non-RTL keywords missing from our subset can serve in simulation test benches (force, release, forever), at the board level in system models (supply0, supply1), or in gate-level models (primitive, and many others). Only the verifiable subset, however, is allowed inside the ASIC's RTL.

Designers can also make rare exceptions for looping constructs within library elements or special circumstances by isolating or abstracting the loop into a simple module. To simplify tool support, however, designers should select only one of the three Verilog looping constructs for a given project. We have chosen the for construct for our looping exception.

In general, a single design decision pertaining to functional complexity should be isolated and localized within a module.

In our verifiable subset, we support 30 out of the 35 Verilog expression operators. The remaining five Verilog operatorsýunary minus (-), multiply (*), divide (/), equality (===), and inequality (!==)ýhave been excluded from our simplified RTL Verilog coding style.

Designers can make an exception with the first three operators when they are isolated from the standard RTL Verilog descriptions. In general, a single design decision pertaining to functional complexity should be isolated and localized within a module. Isolating the functional complexity of multipliers is a classic example of how RTL coding considerations can improve the equivalence checker's runtime performance. The module's ports should clearly identify the complex function's boundaries and permit the equivalence-checking tool to try out different architectures for the multiplier to improve its runtime performance.

Removing the lint

A linting strategy targeted as an initial check in the complete line of verification tools is the initial and most cost-effective method of finding design errors. In addition to identifying syntax errors and project-specific coding rule violations, verification-oriented linting makes design and analysis toolsýas well as engineering teamsýmore productive. Hence, we always establish a linting methodology early in our design cycle, and use it to enforce all verifiable subset and project-specific coding style requirements and rules. Historically, we have written our own project-specific linting tool to enforce compliance with our verifiable subset, coding style, and additional checks. For example, we have elevated mismatched widths across expression operators as errors within our linting tool. Many commercial linting tools available today permit teams to extend their tool's checks for project specific needs.

We actually embed our linting process directly in the design flow (in makefiles, for example), and use it to prevent the advancement to subsequent processes within the flow upon detection of errors or code style violations. Enforcing a project-specific coding style allows us to achieve a truly verifiable RTL design.

In the early 1990s, the system design communities underwent tremendous productivity gains in gate-level design as engineers embraced synthesis technology. Unfortunately, this resulted in an increase in the verification problem space for the design as well as the overall validation effort. To keep up with escalating design complexity and size, the Hewlett-Packard lab has emphasized the development of a Verilog RTL coding style and a verifiable subset to optimize our verification flow. By constraining the RTL to a verifiable subset, we have succeeded in augmenting cycle-based simulation, 2-state simulation, formal equivalence checking, and model checking into our traditional verification flow. A verifiable RTL coding style allows us to achieve greater verification coverage in minimal time, enhances cooperation and support for multiple EDA tools within the flow, clarifies RTL design intent, and facilitates emerging verification processes. The technique has effectively reduced development time-to-market while simultaneously achieving a higher level of verification confidence in our final products.