Kai-Chun (Kevin) Chang

Simulation-based falsification has proved to be an effective verification method for cyber-physical systems. Traditional approaches to falsification take as input a single or a set of temporal properties that must be satisfied by the system at all times. In this paper, we consider falsification of a more complex specification with two dimensions: multiple objectives with relative priorities and the evolution of these objectives characterized by time-varying priorities. We introduce the concept of dynamic rulebooks as a way to specify a prioritized multi-objective specification and its evolution over time. We develop a novel algorithm for falsifying a dynamic rulebook specification on a cyber-physical system. To evaluate our approach, we define scenarios and dynamic rulebook specifications for the domains of autonomous driving and human-robot interaction. Our experiments demonstrate that integrating dynamic rulebooks allows us to capture counterexamples more accurately and efficiently than when using static rulebooks. Moreover, our falsification framework identifies more numerous and more significant counterexamples as compared to previous approaches.

Timing macro modeling has been widely employed to enhance the efficiency and accuracy of parallel and hierarchical timing analysis. However, existing studies primarily focused on generating an accurate and compact timing macro model for single-corner libraries, making it difficult to adapt these approaches to multi-corner situations. This either incurs substantial engineering effort or results in significant performance degradation. To tackle this challenge, we offer a fresh perspective on the timing macro modeling problem by drawing inspiration from recommendation systems and formulating it as a matrix completion task. We propose a neural collaborative filtering-based framework capable of capturing the convoluted relationships between circuit pins and timing corners. This framework enables the precise identification of timing variant regions across different corners. Additionally, we design several training features and implement various training techniques to enhance precision. Experimental results show that our framework reduces model sizes by more than 10% compared to state-of-the-art single-corner approaches, while maintaining competitive timing accuracy and exhibiting significant runtime improvements. Furthermore, when applied to unseen corners, our framework consistently delivers superior performance, demonstrating its potential for use in off-corner chiplets in a heterogeneous integration system.

Neural-network-based (NN-based) planners have been increasingly used to enhance the performance of planning for autonomous vehicles. However, it is often difficult for NN-based planners to balance efficiency and safety in complicated scenarios, especially under real-world communication disturbance. To tackle this challenge, we present a safety-guaranteed framework for NN-based planners in connected vehicle environments with communication disturbance. Given any NN-based planner with no safety-guarantee, the framework generates a robust compound planner embedding the NN-based planner to ensure overall system safety. Moreover, with the aid of an information filter for imperfect communication and an aggressive approach for the estimation of the unsafe set, the compound planner could achieve similar or better efficiency than the given NN-based planner. A comprehensive case study of unprotected left turn and extensive simulations demonstrate the effectiveness of our framework.

Due to rapidly growing design complexity, timing macro modeling has been widely adopted to enable hierarchical and parallel timing analysis. The main challenge of timing macro modeling is to identify timing variant pins for achieving high timing accuracy while keeping a compact model size. To tackle this challenge, prior work applied ad-hoc techniques and threshold setting. In this work, we present a novel timing macro modeling approach based on graph neural networks (GNNs). A timing sensitivity metric is proposed to precisely evaluate the influence of each pin on the timing accuracy. Based on the timing sensitivity data and the circuit topology, the GNN model can effectively learn and capture timing variant pins. Experimental results show that our GNN-based framework reduces 10% model sizes while preserving the same timing accuracy as the state-of-the-art. Furthermore, taking common path pessimism removal (CPPR) as an example, the generality and applicability of our framework on various timing analysis models and modes are also validated empirically.