• Posted by: Technology Staff Editor
• In: Information Technology

» Add a Comment  Send to Friend

BENGALURU, India — Two engineers at Oski Technology Inc. (Fremont, Calif.) have demonstrated a formal verification planning process and associated verification strategy that they say is a necessary—though often ignored—step in an ASIC or SoC functional formal verification flow.

In a paper presented at a recent conference here, the pair described a way to apply the verification planning process and set of abstraction techniques on the Sun OpenSparc DDR2 controller. The process and verification strategy apply in particular to DDR2 controllers but can be generalized for other designs, they said.

Model checking (formal verification) usage has risen as formal engines have increased in performance and capacity, and as property specification languages have been standardized. But formal verification still cannot lay claim to mainstream acceptance as a necessary part of verification signoff, mainly owing to a dearth of published material on three key aspects of effective formal verification: structured verification planning, reusable verification intellectual property (IP) and good verification strategies.

Oski engineers Abhishek Datta and Vigyan Singhal acknowledged in their presentation that many efforts have addressed verification planning and that formal verification IP reuse has been reasonably well-documented. But they argued that "there remains a need to disseminate effective verification strategies and methods to simplify complexity without necessarily compromising the completeness of the desired proof. Without good strategy, most formal verification projects will be overwhelmed by complexity issues."

The pair noted that "most memory controllers have common design strategies, even though they have been designed independently. This is partly because common design techniques permeate the industry over time and partly because of the requirements imposed by the standard specifications.

"Therefore, we believe that the complexity issues described are pertinent to most DDR controller implementations. By extension, the techniques used to tackle the complexity are applicable to the whole class of memory controller designs and can be leveraged for other design types."

The demonstration involved four on-chip dynamic random-access memory (DRAM) controllers directly interfacing to double-data-rate synchronous DRAM (DDR2 SDRAM) modules. The controllers implemented a 144-bit interface per channel with a 25-Gbyte/second peak total bandwidth. The downloadable package for the chip contained the Verilog RTL source, documentation and a comprehensive simulation-based regression environment.

"We had no access to the designers of the block, and an element of guesswork was involved in constraining the internal interfaces," the engineers stated. "Further, we had to spend more time looking though the RTL than normally required.

"The functional specification of the block and the simulation-based regression infrastructure were well documented. We restricted our efforts to the control path in the controller block. Also, we focused solely on the DDR2 interface properties of the block."

The whole effort took the equivalent of about three weeks for one person working alone, they reported, attributing the much-shortened schedule mainly to the availability of DDR2 verification IP and good documentation.

Presenting elements of verification strategy for a DDR2 controller design, the two engineers showed how simulation-assisted initialization; design symmetry exploitation; and the use of cut-points, design abstractions and verification patterns can reduce complexity.

"The techniques and abstractions presented have been found to be equally effective in the verification of other classes of designs," they reported.