A5021812698- Embedded Systems Design Techniques
- Formal Methods in Verification
- VLSI and Analog Circuit Testing
- Software Testing and Debugging Techniques
- Model-Driven Software Engineering Techniques
- Parallel Computing and Optimization Techniques
- Radiation Effects in Electronics
- Software Engineering Research
- Software Reliability and Analysis Research
University of California, Berkeley
2018-2024
Berkeley College
2022
University of California System
2018
Dynamic verification is widely used to increase confidence in the correctness of RTL circuits during pre-silicon design phase. Despite numerous attempts over last decades automate stimuli generation based on coverage feedback, Coverage Directed Test Generation (CDG) has not found widespread adoption that one would expect. Based new ideas from software testing community around coverage-guided mutational fuzz testing, we propose a approach CDG problem which requires minimal setup and takes...
In software and hardware testing, generating multiple inputs which satisfy a given set of constraints is an important problem with applications in fuzz testing stimulus generation. However, it challenge to perform the sampling efficiently, while diverse constraints. We developed new algorithm QuickSampler requires small number solver calls produce millions samples high probability. evaluate on large real-world benchmarks show that can unique valid solutions orders magnitude faster than other...
With the current ever-increasing demand for performance, hardware developers find themselves turning ever-more towards construction of application-specific accelerators to achieve higher performance and lower energy consumption. In order meet ever-shortening time constraints, both development verification tools need be improved. Chisel, as a language, tackles this problem by speeding up digital designs. However, Chisel infrastructure lacks verification. This paper improves efficiency in...
We demonstrate a new approach to implementing automated coverage metrics including line, toggle, and finite state machine coverage. Each metric is implemented through compiler pass with report generator. They are decoupled from the backend simulation, emulation, or formal verification tool simple API designed around single cover primitive. Our prototype for Chisel hardware construction language demonstrates support across three software simulators, FPGA-accelerated FireSim simulator tool....
FPGA prototyping has long been an indispensable technique in pre-silicon verification as well enabling early-stage software development. FPGAs themselves have also gained popularity hardware accelerators deployed datacenters. However, development brings a plethora of problems. These issues constitute high barrier towards mass adoption agile surrounding FPGA-based projects.
UCLID5 is a tool for the multi-modal formal modeling, verification, and synthesis of systems. It enables one to tackle verification problems heterogeneous systems such as combinations hardware software, or those that have multiple, varied specifications, require hybrid modes modeling. A novel aspect \uclid an emphasis on use syntax-guided inductive automate steps in modeling verification. This paper presents new developments including language features, integration with techniques...