|
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 synchronousDRAM (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.
The work presented is in the public domain. The design and verification material can be downloaded from the Formal Verification Patterns repository.
Read the original article: http://www.eetimes.com/news/latest/showArticle.jhtml?articleID=208404220
 |
Get Informed 
Subscribe to this comment's feed
Show/Hide comments