In probabilistic program analysis, quantitative analysis aims at deriving tight numerical bounds for probabilistic properties such as expectation and assertion probability. Most previous works consider numerical bounds over the whole program state space monolithically and do not consider piecewise bounds. Not surprisingly, monolithic bounds are either conservative, or not expressive and succinct enough in general. To derive better bounds, we propose a novel approach for synthesizing piecewise bounds over probabilistic programs. First, we show how to extract useful piecewise information from latticed 𝑘-induction operators, and combine the piecewise information with Optional Stopping Theorem to obtain a general approach to derive piecewise bounds over probabilistic programs. Second, we develop algorithms to synthesize piecewise polynomial bounds, and show that the synthesis can be reduced to bilinear programming in the linear case, and soundly relaxed to semidefinite programming in the polynomial case. Experimental results show that our approach generates tight piecewise bounds for a wide range of benchmarks when compared with the state of the art.

With technology scaling progressing well into deep nanometer region, the number of technology corners surges from dozens to hundreds. This dramatic increase in corners significantly complicates timing closure during Engineering Change Orders (ECO) stages, as performing full-corner static timing analysis (STA) becomes increasingly time-consuming and challenging. Existing methodologies often leverage machine learning (ML) techniques to predict unknown corners based on a subset of known corners. However, as the total number of corners expands, these methods not only require a larger set of known corners but also become highly sensitive to known corner selection. Additionally, as designers push designs into near-threshold voltage regions to enhance energy efficiency, the number of corners increases and the nonlinearity between corners becomes more pronounced. This intensifies the difficulty for current ML-based methods to accurately predict full-corner timing metrics. In this work, we propose FACT, a fast and accurate multi-corner predictor for timing closure optimization. Our approach simplifies the process by necessitating timing analysis under only one known corner. By effectively capturing correlations across diverse technology files, FACT robustly infers full-corner timing metrics, even under challenging near-threshold conditions. Moreover, our framework seamlessly integrates with commercial EDA design flows, making it practical in industrial environments. Experimental results on open-source designs indicate the superior stability of our method, coupled with a significant runtime speed-up over both traditional and prior ML-based timing ECO flows.

Coarse-Grained Reconfigurable Arrays (CGRAs) are a promising architecture that warrants thorough design space exploration (DSE). However, traditional DSE methods for CGRAs often get trapped in local optima due to singularities, i.e., invalid design points caused by CGRA mapping failures. In this paper, we propose a singularity-aware framework based on the integration of reinforcement learning (RL) and imitation learning (IL) for DSE of CGRAs. Our approach learns from both valid and invalid points, substantially reducing the probability of sampling singularities and accelerating the escape from inefficient regions, ultimately achieving high-quality Pareto points. Experimental results demonstrate that our framework improves the hypervolume (HV) of the Pareto front by 23.56% compared to state-of-the-art methods, with a comparable time overhead.