EDA² | ISEDA 2025 | Technical Session

Innovative Simulation and Data Compression for Verification

Session Chair: Hongce Zhang, The Hong Kong University of Science and Technology (Guangzhou)

Abstract: In streaming applications the robustness against small deviations can be exploited to minimize crosstalk effects. In this contribution it is shown how approximation for crosstalk avoidance can be efficiently integrated with error detection.

Abstract: Formal verification has become increasingly challenging as integrated circuits continue to grow in complexity. This approach translates hardware description languages into Satisfiability Modulo Theories (SMT) formulas and employs existing SMT solvers for verification. However, current hardware formal verification methodologies typically treat these solvers only as back-end components, which often fails to capture underlying information, thus limiting their performances. To address the concern, this paper introduces ITE-PBA, a novel framework that enhances SMT solving by leveraging If-Then-Else terms originating from data selectors and exploiting their embedded control flow information. In addition, a parallel branching assignment strategy simultaneously applies multiple mainstream and classical assignment schemes, improving the likelihood of identifying effective solutions. Experimental results reveal that integrating ITE-PBA into the Yices2 solver yields speedups of 9.46×.

Abstract: This paper proposes a VCD file compression method based on signal function relationships, signal value prediction, and bit-plane reorganization. The method aims to address the bottleneck issues related to the storage and transmission of VCD files as the scale of integrated circuit designs continues to grow. The paper develops separate compression strategies for different sections of the VCD file, such as the header, node information, and value change sections, in order to enhance compression efficiency. By analyzing the functional relationships between signals in the value change section and integrating techniques including variable-length encoding, signal value prediction, and bit-plane reorganization, the proposed method significantly improves the compression ratio. The experimental results demonstrate that, for KB-level VCD files, the compression ratio of the method proposed in this paper reaches twice that of other methods. For MB-level files, the compression ratio can reach up to 86.9 times, representing a 142% improvement over existing compression algorithms. Additionally, this paper also addresses special cases, such as the handling of keywords like "$dumpon", ensuring comprehensive optimization and correctness of the compressed VCD files.

Abstract: Accurate timing analysis is crucial for design and verification. In addition, high throughput and scalability are mandatory for simulation-based approaches, which must often cope with high input data volumes and a high number of large circuit instances. Existing approaches using a binary switch model offer an excellent trade-off between accurate SPICE and high-performance gate level simulation in planar CMOS. However, recent experiments have shown that the binary switch model is not accurate enough for FinFET technology. The new approach presented in this paper integrates an enhanced switch-level model into an efficient GPU-based simulation flow. A high throughput is achieved by avoiding event-driven control at the top level, enabling the thread-parallel processing of independent components and input patterns. Experimental results confirm that the new approach accrately predicts the timing of digital circuits in modern CMOS technologies and scales well to multi-million transistor designs..