Design Automation and Verification Group
Overview
Members of the Design Automation and Verification (DAV) Group share a common interest in the specification, design, analyisis and verification of both software and hardware systems. Current research interests include:- formal models of interconnect protocols for system-on-chip architectures
- techniques for formal verification and performance analysis
- feedback-based approaches for coverage-directed stimulus generation (for simulation-based verification)
- static analysis of systems using abstract interpretation
- equivalence checkers based on ATPG techniques such as Recursive Learning
- SAT solvers based on structural techniques
- techniques for verification of performance and power in chip designs
The group aims to expand its research activities into system-level functional verification techniques both formal and simulation based. We have long established links with a number of local and international companies such as Infineon, STMicroelectronics, Broadcom, Cadence and IBM, who provide some of their designs or tools for collaborative research projects.
We plan to expand the verification research, for timing optimization and performance/power verification. Low-power designs provide the major challenges for the chip design in the future. What we are exploring here is power estimation technique for both combinational and sequential logic, as well as power optimization techniques. Additionally being explored here are new approaches to SAT-solvers - a fundamental problem in computer science. This has many applications to CAD as well as to verification.
Achievements
- Developed approach for the design and verification of microprocessor pipelines which allowed reasoning about timing and performance as well as functional correctness.
- Developed Equivalence Checker for Mentor Graphics Proformal .
- Introduced the concept of uniform framework for synthesis, test and verification based on Recursive Learning.