Computing a perfect input assignment for probabilistic verification
2005 (English)In: VLSI Circuits and Systems II, Pts 1 and 2 / [ed] Lopez, JF; Fernandez, FV; LopezVillegas, JM; DelaRosa, JM, BELLINGHAM: SPIE-INT SOC OPTICAL ENGINEERING , 2005, Vol. 5837, 929-936 p.Conference paper (Refereed)
Design verification is the task of establishing that a given design meets the intended behavior. The growing complexity of verification instances requires new methods that can provide high quality verification coverage for large, complex designs. Probabilistic verification complements existing simulation-based and formal verification techniques by providing a distinct trade-off between coverage and capacity. Probabilistic approach maps two Boolean functions onto hash values and compare these values for equivalence. The major drawback of probabilistic verification is the non-zero probability of collision of hash values of two non-equivalent functions, producing "false positive" verification results. In this paper, we prove the existence of a perfect input assignment which never causes collisions. We show that the equivalence of hash values computed for a perfect input assignment implies the equivalence of functions with 100% probability.
Place, publisher, year, edition, pages
BELLINGHAM: SPIE-INT SOC OPTICAL ENGINEERING , 2005. Vol. 5837, 929-936 p.
, PROCEEDINGS OF THE SOCIETY OF PHOTO-OPTICAL INSTRUMENTATION ENGINEERS (SPIE), ISSN 0277-786X ; 5837
probabilistic verification; arithmetic transform; perfect input assignment
Atom and Molecular Physics and Optics
IdentifiersURN: urn:nbn:se:kth:diva-43008DOI: 10.1117/12.607828ISI: 000231723000095ScopusID: 2-s2.0-28344448722ISBN: -8194-5832-5OAI: oai:DiVA.org:kth-43008DiVA: diva2:447724
Conference on VLSI Circuits and Systems II . Seville, SPAIN. MAY 09-11, 2005
QC 201110132011-10-132011-10-132012-11-01Bibliographically approved