Home » Research Projects

Research Projects

Automated Verification and Debugging using Formal Methods

In our past projects, we proposed a novel verification technique using Gröbner basis theory to formulate the equivalence checking problem as an ideal membership testing in the algebraic domain and achieve an efficient verifier. This approach is capable of identifying bugs in a deterministic way since word-level representations are utilized.

Existing equivalence checking techniques utilize Gröbner basis theory to produce a remainder to indicate the presence of a potential bug. However, bug localization remains a major bottleneck. Simulation-based validation using random or constrained-random tests are not effective and can be infeasible for complex arithmetic circuits. In our past projects, we developed an automated test generation and bug localization technique for debugging arithmetic circuits. Our approach is able to automatically generate directed tests by suitable assignments of input variables to make the reminder non-zero. The generated tests are guaranteed to activate the unknown bugs. We also proposed a bug detection and correction technique by utilizing the patterns of remainder terms as well as the intersection of regions activated by the generated tests. In her recent work, we have addressed the scalability concerns associated with equivalence checking that leads to an explosion in size of the remainder when the design is faulty. We developed an incremental equivalence checking method which is capable of localizing and correcting hard-to-detect bugs irrespective of their location in the design. In our current project, we plan to use Grobner basis theory for approximate hardware generation and its automatic debugging.

Related Publication:


Design Automation of Modeling IoT Devices

Design of IoT devices starts with a high-level model of Internet-of-Things (IoT) devices as well as their constraints. Modeling of heterogeneous IoT devices, as well as their connectivity, is a major challenge due to the huge complexity coupled with the diversity of the computing models. After models and constraints are finalized, they should be validated and converted to actual hardware using efficient design exploration, fast prototyping, and effective design transformations. This modeling and validation would lead to the development of novel Electronic Design Automation (EDA) tools to enable automated generation of executable models and prototypes for CMOS as well as post-CMOS technologies. My future research aims for correct-by-construction design automation methodology. In this project, we design EDA tools that generate high-level models based on the design constraints and perform verification of transformation steps from models to hardware chips. The automated framework would enable design exploration, automatic software generation, high-level synthesis, quick prototyping, and automatic patching. It is also extremely important to have EDA tools that can check for all vulnerabilities in all phases of the design since it may be infeasible to patch later. The tools must be able to predict various vulnerabilities such as reverse engineering, and fault injection attacks with warnings and possible solutions.

Related Publications:

Verification of IoT System-on-Chips

Modern SoC design technology has been a centerpiece in computing system architecture because of diverse applications such as smartphones, tablets, automotive systems, medical instruments, etc. It is very important to design robust and trustworthy SoCs. In this project, we plan to explore the following avenues to verify IoT SoCs, 1) use of analytics, formal validation, as well as machine learning techniques for scalable validation, and 2) streamlined architecture for effective post-silicon and in-field control and requirements update. Faster bug localization is one of the most important steps in design validation. A major problem with design validation is that we do not know whether a bug exists, and how to quickly detect and fix it. In this project, we use machine learning to implement verification tools that automatically detect the source of errors based on prior knowledge and verification efforts. The goal of this research is to reduce validation efforts by avoiding debugging known failures. In this project, we also plan to generate test patterns using machine learning. While directed tests can check for known errors, machine learning can extend to scope for both known and unknown (e.g., known errors with minor or major variations) SoC functional vulnerabilities.

We also aim for effective utilization of three widely used formal methods (equivalence checking, model checking, and theorem proving) for scalable validation techniques.  Effective in-field debug should be performed in the case of buggy fabricated silicon. Post-silicon validation and debug is critical for IoT applications, where the device may need to be updated during its long lifetime, or in response to changing functional needs or new requirements.

Related Publication:

Post-Silicon Validation and Debug

Post-silicon validation is widely acknowledged as a major bottleneck for complex System-on-Chip (SoC) designs. Recent studies suggest that post-silicon validation consumes more than 50% of a SoC’s overall design effort (total cost). Due to the practically infinite design space complexity as well as shrinking time-to-market, many bugs in a large SoC are highly likely to evade conventional post-silicon validation.

In our past project, we proposed novel post-silicon validation techniques to ensure the correct behavior of silicon designs based on coverage analysis. Currently, there is no effective way to collect coverage of certain properties and events directly and independently on silicon. We explored how to utilize on-chip designfor– debug (DfD) infrastructure (e.g., trace buffer and scan chain) to improve observability of assertions. This analysis enables us to identify a small percentage of coverage monitors that need to be synthesized in order to provide a trade-off between observability of design properties versus design overhead. The result of this work is also used for an efficient signal selection to improve coverage analysis without compromising on debug observability.

There is an inherent conflict between increasing the observability and trust. Although designing effective debug infrastructures can drastically reduce the post-silicon validation and debug efforts by increasing the observability, the extra observability can facilitate integrity issues such as trace buffer attack and scan-based side channel attack. We plan to explore designing debug infrastructures that they do not violate any integrity constraints.

Related Publications: