主 题: Automated Venification with Abstract Data
报告人: Song Xiaoyu, Professor (Department of Electrical & Computer Engineering)
时 间: 2007-09-13 下午 2:00 -
地 点: 理科一号楼 1560
Traditional ROBDD-based methods of automated verification
suffer from the drawback that they require a binary representation of
the circuit. To overcome this limitation we propose a broader class of
decision graphs, called Multiway Decision Graphs (MDGs), of which ROBDDs
are a special case. With MDGs, a data value is represented by a single
variable of abstract type, rather than by 32 or 64 boolean variables,
and a data operation is represented by an uninterpreted function symbol.
The MDGs represent and manipulate a subset of first-order logic formulas
suitable for high-level hardware verification. The talk addresses
MDG-based verification methods in terms of implicit state enumeration of
abstract descriptions of state machines (ASM).
Bio:
Xiaoyu Song received his Ph.D. degree in Computer Science from
University of Pisa, Italy, 1991. From 1992 to 1999, he was on the
faculty of the Department of Computer Science at the University of
Montreal, Canada. Since 1999 he has been a professor in the Department
of Electrical & Computer Engineering at Portland State University. His
research interests include formal verification for hardware and software
systems, design automation, high performance digital system designs, and
optimization. He has been awarded as Intel Faculty Fellow during
2000-2005. He served as an associate editor of IEEE Transactions on
Circuits and Systems and IEEE Transactions on VLSI Systems.
