Design Verification Techniques

Tarachand Pagarani

With Rapid Evolution of VLSI Technology, modern hardware Designs have become increasingly large and complex. Guaranteeing the correctness of designs and detection and removal of design errors early in the design cycle is extremely important.Discovery of these errors after fabrication could require a costly redesign and re-fabrication. During the design of a system from higher level to lower level we have to ensure the functionality of the system. To see that a given system before and after various design steps is functionally same we need automatic verification tools.

Verification can be done by simulation only but in case of large design this method is not time effective. In this case designer's knowledge of the circuit is very important. Verification of the gate level system poses a serious problem. There is still research going on in this field. I am going to present some of the methods currently being used for verification. These techniques are broadly classified into three categories.

1)Techniques in which circuit is unchanged e.g. HANNIBAL, OBDD based methods etc.These methods rely on the structural similarities between circuits before and after the optimization process.First they combine the inputs of the circuit and feed their output to a XOR gate. Now verification problem reducesto satisfiability problem.They use recursive learning to obtain correspondence between nodes of the circuits.Then these learnings are used during ATPG to find the test vector to prove Stuck-at-0 fault at the ouput of XOR gate to be redundant.This approach is suitable for circuits which have lots of structural similarity.For large circuits OBDD based approach may cause memory explosion.

2)In which circuit is reduced. This approach uses same learning approach but replaces equivalent nodes by primary inputs. This seems to be very simple approach but it is plagued by false negatives.

3)In which size of both circuit under Verification (CUV) and reference circuit(RF)may increase. This approach locates the dissimilar regions in composite circuit and then applies some transformations to introduce similarities between them.This approach seems contrary to usual thinking that increase in circuit size makes it more difficult to verify but along with the increase in size this approach improves correpondence between two circuits hence improves verification possibility. However this approach is not time efficient in locating dissimilar regions.

(1)VERILAT: Verification Using Logic Augmentation and Transformations By Dhiraj K. Pradhan, Debjyoti Paul, Mitrajit Chatterjee. ICCAD 96,PP. 88-95.

(2)HANNIBAL: An Efficient Tool For Logic Verification Based on Recursive Learning By W. Kunz. International Conference On CAD,1993 ,pp.538-543.

(3)Advanced Verification Techniques Based on Learning By J.Jain, R.Mukherjee M.Fujita. Design Automation Conference,1995,pp.420-426.

Here is a link back to the ECMP 486 Home Page.

Joan Carletta, carletta@ces.cwru.edu