Formal
and semi-formal verification 
Symbolic simulation in
verification of embedded array systems and arithmetic unit
|
|
|
| Embedded memory arrays and
arithmetic units are important components in digital ICs for most
high-performance applications. Both of them have the difficulties
for verification. In our project, we provide several methods to target
them. Enhanced symbolic simulation based on collapsing and decomposition
is the crucial way to avoid the OBDD size explosion during the
verification. Self-referential equivalence checking is another
method to improve the efficiency.
|
|
| |
| Symbolic methods in
efficient validation of embedded memory arrays |
| We incorporate an ATPG-style decision procedure into the
symbolic simulation. To verify that a design satisfies a given assertion,
the assertion is modeled as a constraint circuit. ATPG assigns the
constant values through the backward justification, and symbolic simulation
can simulate the sub-assertions with efficient encoding. |
| |
| For the content-addressable memory, we explore the similarity of the
word-level functions between the design and assertions. Some OBDD
sub-trees can be collapsed into a new variable, so the output OBDD sizes
are dramatically reduced during the simulation. |
| |
Publications:
• G. Parthasarathy, M. K. Iyer, T. Feng, L.-C. Wang, K.-T. Cheng and
M. S. Abadir, "Combining
ATPG and Symbolic Simulation for Efficient Validation of Embedded Array
Systems," in Proc. Int. Test Conf., pp. 203-212, Oct.
7-10, 2002.
• T. Feng, Li-C. Wang, K.-T. Cheng, M. Pandey and M. S. Abadir,
"Enhanced
Symbolic Simulation for Efficient Verification of Embedded Array Systems,"
in Proc. Asia and South Pacific Design Automation Conf.,
pp.302-307, Jan. 21-24, 2003. |
|
|
| Enhanced Symbolic simulator
with functional space decomposition |
| We use
functional-space
decomposition to improve the symbolic simulator. The datapath and control
logic of a circuit is separated, and their corresponding functions are
recorded in two different domains by a special structure called 2-tuple
list. The functional space in the control domain can further be decomposed
into subspaces during the simulation to achieve the optimal OBDD size and
run time. |
| |
| Our decomposition is based on the decision points implicitly
built inside the circuit. We apply some heuristics to extract and choose
the decision points automatically. The effectiveness of the approach is
demonstrated on the arithmetic circuits and the memory management unit. |
| |
Publications:
• Tao Feng, Li-C. Wang, Kwang-Ting Cheng, "Improved Symbolic
Simulation By Functional Space Decomposition", to appear in Asia and
South Pacific Design Automation Conference (ASP-DAC), Jan, 2004.
• Tao Feng, Li-C.Wang, Kwang-Ting Cheng, C.C.Lin, "Improved
Symbolic Simulation By Dynamic Functional Space Partitioning", to
appear in Design, Automation and Test in Europe (DATE), Feb, 2004. |
| |
| Self-referential verification of
arithmetic circuits |
| We propose a self-referential
verification approach which makes use of the gate-level implementation to
verify itself without referencing to a standard. Specifically, for the
arithmetic operator on the binary vector numbers, the successive
unrolling induction in bit step can decompose the verification task into a
sequence of equivalence-checking sub-problems. |
| |
| In each sub-problem, both circuits to be compared are derived from the same circuit and have
significant structural similarities. This approach could be integrated
into a generic equivalence-checking engine for more efficient datapath
verification. |
| |
Publications:
• Y.-T. Chang and K.-T. Cheng, "Induction-based
Gate-Level Verification of Multipliers," in Proc. Int. Conf.
on Computer-Aided Design, pp. 190-193, Nov. 4-8, 2002.
• Y.-T. Chang and K.-T. Cheng, "Self-Referential
Verification of Gate-Level Implementations of Arithmetic Circuits,"
in Proc. Design Automation Conf., pp. 311-316, Jun. 10-14,
2002. |