Welcome to the VLSI CAD LAB at the Dept. of Electrical and Computer Engineering at the University of Massachusetts Amherst. This group is led by Prof. Maciej Ciesielski. Electronic Design Automation for digital systems. Formal methods in Computer-Aided Design. Behavioral and RTL synthesis. Formal verification and design validation.

Professor Ciesielski is Associate Department Head (since Sept. 2006), ECE Graduate Seminar Committee, ECE Personnel Committee, ECE Department Accreditation ABET Task Force, Member of Technical Program Committees at several international conferences and workshops (VLSI, ICCAD, IWLS, ECECS, CFV), Session and Topic Chair at DAC 2006, CFV 2008.


  • Electronic Design Automation (EDA): CAD tools and algorithms.
  • Formal verification; functional verification of arithmetic circuits.
  • Simulation-based design validation; parallel simulation.
  • Behavioral and logic synthesis from high-level specifications.
  • Mathematical optimization.

    Software Release

  • BDS ( BDD-based Logic Synthesis system)
  • TDS (TED-based Synthesis and Verification System )
  • Parallel Simulation
  • ABL Verification System
  • Research Projects

    BDS (BDD-based Logic Synthesis system)

    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.

    Source code of BDS-1.2 is now available upon request for non-commercial, academic use only. Please contact Prof. Maciej Ciesielski at ciesiel@ecs.umass.edu to obtain the code.

    TDS: A Behavioral Transformation System based on Canonical Dataflow Representation

    TDS is an experimental software tool for behavioral transformations of designs specified on algorithmic and behavioral levels. It 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), and are followed by structural transformations of the resulting DFG network. The system is intended for data-flow and computation-intensive designs used in digital signal processing applications.

    ABL Function Computing

    These works investigate formal verification for arithmetic bit-level circuits (ABL). The circuit is modeled as a network of adders and basic Boolean gates, and the computation performed by the circuit is viewed as a flow of binary data through such a network. The verification problem is cast as a Network Flow problem and solved using symbolic term rewriting and simple algebraic techniques. Functional correctness is proved by showing that the symbolic flow computed at the primary inputs is equal to the flow computed at the primary outputs. Experimental results show a potential application of the method to certain classes of arithmetic circuits.

    Parallel Simulation

    In the area of multi-core computing, the push for creating true parallel applications that can run on individual CPUs is on the rise. Application of parallel discrete event simulation (PDES) to hardware design verification looks promising, given the complexity of today’s hardware designs. Unfortunately, the challenges imposed by lack of inherent parallelism, suboptimal design partitioning, synchronization and communication overhead, and load balancing, render this approach largely ineffective.

    This work presents three techniques for accelerating simulation at three levels of abstraction namely, RTL, functional gate-level (zero-delay) and gate-level timing. We review contemporary solutions and then propose new ways of speeding up simulation at the three levels of abstraction. We demonstrate the effectiveness of the proposed approaches on several industrial hardware designs.