In this talk, I will present a suite of techniques that are a significant departure
from traditional Boolean level approaches to formal verification. The algorithms
are based on a top-down, domain-aware perspective of the system by reasoning at
the system level and register transfer level descriptions. Static analysis of
these high level system descriptions using structural information and symbolic
reasoning leads to effective decomposition strategies that create tractable portions
of the system. These manageable system components can then be verified by deploying
efficient Boolean level algorithms. Since the focus of this research is toward
increasing practical applicability of formal verification, I will illustrate my
techniques with respect to their efficacy in solving real, challenging verification
problems. I will discuss antecedent conditioned slicing and its application to
property checking in the context of embedded processor verification. I will also
discuss comparison point theory for Hardware Description Languages and its application
to equivalence checking in the context of multiplier and SoC verification.
BIOGRAPHY
Shobha Vasudevan has joined this semester as an Assistant Professor in the
ECE department. She got her Ph.D. in December 2007 from The University of Texas
at Austin. She received an M.S.E. degree in Computer Engineering in 2003 from
The University of Texas at Austin, and a B.E. degree from the University of
Mumbai, India. Her research interests are in formal and semi-formal verification
of VLSI and embedded systems, VLSI and SoC testing, system level power management
and software verification.