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.
- Automated test generation for debugging multiple bugs in arithmetic circuits
- Automated Debugging of Arithmetic Circuits Using Incremental Gröbner Basis Reduction
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.
- Security-aware FSM Design Flow for Identifying and Mitigating Vulnerabilities to Fault Attacks
- FSM Anomaly Detection Using Formal Analysis
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.
Post-Silicon Validation and Debug
Post-silicon validation is widely acknowledged as a major
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
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.