Tel: (413) 545-0401
- Ph.D., University of Rochester, 1984.
- M.S., Warsaw Technical University, 1974
- 1986-present, University of Massachusetts, Amherst.
- 1983-1986, GTE Laboratories, Waltham, MA;
Doctorate Honoris Causa , Universite de Bretagne Sud, Lorient, France, 2008.
- First-Year Experience Student Choice Award, University of Massachusetts Amherst, 2013.
Electronic Design Automation (EDA): CAD tools and algorithms.
VLSI CAD Laboratory
- Formal hardware verification.
- Functional verification of arithmetic circuits.
- Behavioral and logic synthesis.
Open RA Position
I have an open RA position for a PhD candidate in the area of hardware verification, and specifically in formal verification of arithmetic circuits.
Successful candidate must have documented experience in computer programming (C, C++), solid background in computer algorithms, and some knowledge of computer arithmetic. Basic knowledge in computer-aided design for electronic circuits (also known as electronic design automation, EDA) is desirable. The selected person will take the course in Synthesis and Verification of Digital Systems, ECE 667, in Spring 2017.
The qualified candidates interested in this position should send email with a CV to
with the subject matter: "Interested in RA position in formal verification".
Please check the following websites to get yourself familiarized with the type of problems the research entails.
Publications and Slides
A set of selected research papers
presentation slides and tutorials.
is an experimental software tool to perform behavioral transformations of designs specified on algorithmic and behavioral levels. TDS transforms the initial design specifications into a data flow graph (DFG) optimized for a particular objective (latency, resource utilization, etc.) prior to high-level synthesis. The behavioral transformations are based on graph-based canonical representation, Taylor Expansion Diagram (TED), followed by structural transformations of the resulting DFG network.
Thanks to canonicity of the TED representation, the system can be also used for equivalence checking of designs specified in C or behavioral HDL.
The system is intended for data-flow and computation-intensive designs used in digital signal processing applications.
This project was supported by the National Science Foundation under
award No. CCR-0204146 and CCR-0702506 and was done in collaboration with Lab-STICC, Université de Bretagne Sud, Lorient, France.
- BDS (BDD-based Logic Synthesis system)
is our fast and efficient logic synthesis tool, based on a novel theory
of BDD-based bi-decomposition.
It provides both algebraic and Boolean decomposition of several types:
AND, OR, XOR, and MUX.
It handles random and control logic (AND-OR intensive) functions
as well as arithmetic (XOR-intensive) functions.
Its unique approach to partitioned BDD's allows it to handle very large
circuits. Version BDS-1.2 is now available from the following link:
This project has been supported by the National Science Foundation under
grant No. 9901254.
- Cunxi Yu (PhD) - Formal
hardware verification; sequential and floating point arithmetic circuits.
Walter Brown (MS) - Arithmetic verification.
- Ling Zhong (MS)
- Tiankai Su (MS)
About Group, Department and University: