VLDB 2026 Research / reviewers in the wild / expert
Wenji Fang
dblp:345/0547
· DBLP profile ↗
20ranked-venue papers
9as first author
20since 2021 · last 2025
—ORCID · conflict
Domains — the database's venue-derived domains; a paper can count in several
Systems, architecture and hardware · 14 · 7 first-author · 14 since 2021Applied, interdisciplinary, general and emerging computing · 3 · 3 since 2021Artificial intelligence and machine learning · 2 · 1 first-author · 2 since 2021Software engineering, systems software and programming languages · 2 · 1 first-author · 2 since 2021
| Year | Publication | Venue | Position |
|---|---|---|---|
| 2025 | AssertLLM: Generating Hardware Verification Assertions from Design Specifications via Multi-LLMsabstractAssertion-based verification (ABV) is a critical method to ensure logic designs comply with their architectural specifications. ABV requires assertions, which are generally converted from specifications through human interpretation by verification engineers. Existing methods for generating assertions from specification documents are limited to sentences extracted by engineers, discouraging their practical applications. In this work, we present AssertLLM, an automatic assertion generation framework that processes complete specification documents. AssertLLM can generate assertions from both natural language and waveform diagrams in specification files. It first converts unstructured specification sentences and waveforms into structured descriptions using natural language templates. Then, a customized Large Language Model (LLM) generates the final assertions based on these descriptions. Our evaluation demonstrates that AssertLLM can generate more accurate and higher-quality assertions compared to GPT-4o and GPT-3.5. Zhiyuan Yan 0003, Wenji Fang, Mengming Li, Min Li 0019, Shang Liu 0006, Zhiyao Xie, Hongce Zhang |
ASP-DAC | 2 |
| 2025 | A Self-Supervised, Pre-Trained, and Cross-Stage-Aligned Circuit Encoder Provides a Foundation for Various Design TasksabstractMachine learning (ML) techniques have shown remarkable effectiveness in electronic design automation (EDA). Traditionally, most ML for EDA approaches are task-specific, requiring a tedious development process of a tailored ML model for each individual design task. Recently, circuit representation learning has emerged as a promising trend. This approach converts circuits into embeddings, which can then be adapted to distinct downstream tasks. However, existing methods still fall short of providing a truly general circuit representation that supports highly diverse tasks. In this work, we introduce CircuitEncoder, a self-supervised, pre-trained, and cross-stage-aligned general circuit encoder. It provides a general foundation for diverse ML-based EDA tasks, including both design quality and functional reasoning. CircuitEncoder is pre-trained through multi-stage contrastive learning utilizing unlabeled circuits. It encodes circuits from different design stages into embedding vectors within shared latent space, facilitating fine-tuning for various downstream tasks. CircuitEncoder outperforms the state-of-the-art task-specific supervised solutions for multiple EDA tasks, including design quality tasks for register-transfer level (RTL)-stage timing and area prediction, as well as functional tasks for netlist-stage state register identification. Wenji Fang, Shang Liu 0006, Hongce Zhang, Zhiyao Xie |
ASP-DAC | 1 |
| 2025 | Towards Big Data in AI for EDA Research: Generation of New Pseudo Circuits at RTL StageabstractMachine learning (ML) techniques have demonstrated remarkable effectiveness in electronic design automation (EDA). ML models need to be trained on diverse circuit datasets for better accuracy and generalization capabilities. However, the availability of circuit data remains a long-standing severe issue. The strong data privacy concern in the semiconductor industry makes direct sharing of circuit IPs almost impossible. To address the data availability problem, open-source datasets like CircuitNet have been proposed, but they mostly focus on collecting labels of several existing open-source designs, instead of generating any new designs. In this work, we make an innovative exploration to directly generate new pseudo-circuits without human effort. We believe that generating pseudo-circuits is the most promising, if not the only, approach to achieving "big data" in the semiconductor industry in the foreseeable future. We demonstrate that pseudo-circuits can significantly boost the performance of ML models in early design quality predictions, as early as the pre-synthesis RTL stage. Shang Liu 0006, Wenji Fang, Yao Lu 0031, Qijun Zhang, Zhiyao Xie |
ASP-DAC | 2 |
| 2025 | NetTAG: A Multimodal RTL-and-Layout-Aligned Netlist Foundation Model via Text-Attributed GraphabstractCircuit representation learning has shown promise in advancing Electronic Design Automation (EDA) by capturing structural and functional circuit properties for various tasks. Existing pre-trained solutions rely on graph learning with complex functional supervision, such as truth table simulation. However, they only handle simple andinverter graphs (AIGs), struggling to fully encode other complex gate functionalities. While large language models (LLMs) excel at functional understanding, they lack the structural awareness for flattened netlists. To advance netlist representation learning, we present NetTAG, a netlist foundation model that fuses gate semantics with graph structure, handling diverse gate types and supporting a variety of functional and physical tasks. Moving beyond existing graph-only methods, NetTAG formulates netlists as text-attributed graphs, with gates annotated by symbolic logic expressions and physical characteristics as text attributes. Its multimodal architecture combines an LLM-based text encoder for gate semantics and a graph transformer for global structure. Pre-trained with gate and graph self-supervised objectives and aligned with RTL and layout stages, NetTAG captures comprehensive circuit intrinsics. Experimental results show that NetTAG consistently outperforms each task-specific method on four largely different functional and physical tasks and surpasses state-of-the-art AIG encoders, demonstrating its versatility. Wenji Fang, Shang Liu 0006, Yao Lu 0031, Hongce Zhang, Zhiyao Xie |
DAC | 1 |
| 2025 | ATLAS: A Self-Supervised and Cross-Stage Netlist Power Model for Fine-Grained Time-Based Layout Power AnalysisabstractAccurate power prediction in VLSI design is crucial for effective power optimization, especially as designs get transformed from gate-level netlist to layout stages. However, traditional accurate power simulation requires time-consuming back-end processing and simulation steps, which significantly impede design optimization. To address this, we propose ATLAS, which can predict the ultimate time-based layout power for any new design in the gate-level netlist. To the best of our knowledge, ATLAS is the first work that supports both time-based power simulation and general cross-design power modeling. It achieves such general timebased power modeling by proposing a new pre-training and fine-tuning paradigm customized for circuit power. Targeting golden per-cycle layout power from commercial tools, our ATLAS achieves the mean absolute percentage error (MAPE) of only ${0. 5 8 \%, ~} {0. 4 5 \%}$, and ${5. 1 2 \%}$ for the clock tree, register, and combinational power groups, respectively, without any layout information. Overall, the MAPE for the total power of the entire design is $\lt1 \%$, and the inference speed of a workload is significantly faster than the standard flow of commercial tools. Yao Lu 0031, Wenji Fang, Jing Wang 0171, Qijun Zhang, Zhiyao Xie |
DAC | 3 |
| 2025 | SynCircuit: Automated Generation of New Synthetic RTL Circuits Can Enable Big Data in CircuitsabstractIn recent years, AI-assisted IC design methods have demonstrated great potential, but the availability of circuit design data is extremely limited, especially in the public domain. The lack of circuit data has become the primary bottleneck in developing AI-assisted IC design methods. In this work, we make the first attempt, SynCircuit, to generate new synthetic circuits with valid functionalities in the HDL format.SynCircuit automatically generates synthetic data using a framework with three innovative steps: 1) We propose a customized diffusion-based generative model to resolve the Directed Cyclic Graph (DCG) generation task, which has not been well explored in the AI community. 2) To ensure our circuit is valid, we enforce the circuit constraints by refining the initial graph generation outputs. 3) The Monte Carlo tree search (MCTS) method further optimizes the logic redundancy in the generated graph. Experimental results demonstrate that our proposed SynCircuit can generate more realistic synthetic circuits and enhance ML model performance in downstream circuit design tasks. Shang Liu 0006, Jing Wang 0171, Wenji Fang, Zhiyao Xie |
DAC | 3 |
| 2025 | SynC-LLM: Generation of Large-Scale Synthetic Circuit Code with Hierarchical Language ModelsabstractIn recent years, AI-assisted integrated circuit (IC) design methods have shown great potential in boosting IC design efficiency.However, this emerging technique is fundamentally limited by the serious scarcity of publicly accessible large-scale circuit design data, which are mostly private IPs owned by semiconductor companies.In this work, we propose SynC-LLM, the first technique that exploits LLM's ability to generate new large-scale synthetic circuits.Our hierarchical circuit generation process includes three stages: 1) A directed graph diffusion model will learn to generate the skeleton of large circuits with sequential registers.2) The expected function of the input cone of each sequential register will be annotated.Each cone, named flesh, consists of all combinational logic that controls the register value.3) A level-by-level customized prompting technique will guide LLM to complete the design code of each cone.Experiments show that our generated circuits are not only valid and fully functional 1 , but also closely resemble realistic large-scale designs and can significantly improve AI models' performance in multiple IC design tasks.The code and data are open-sourced in https://github.com/hkust-zhiyao/SynCircuitData. Shang Liu 0006, Yao Lu 0031, Wenji Fang, Jing Wang 0171, Zhiyao Xie |
EMNLP | 3 |
| 2025 | GenEDA: Towards Generative Netlist Functional Reasoning via Cross-Modal Circuit Encoder-Decoder AlignmentabstractThe success of foundation AI has motivated the research of circuit foundation models, which are customized to assist the integrated circuit (IC) design process. However, existing pre-trained circuit foundation models are typically limited to standalone encoders for predictive tasks or decoders for generative tasks. These two model types are developed independently, operate on different circuit modalities, and reside in separate latent spaces. This restricts their ability to complement each other for more advanced capabilities. In this work, we present GenEDA, the first framework that cross-modally aligns circuit encoders with decoders within a shared latent space. GenEDA bridges the gap between graph-based circuit representation learning and text-based large language models (LLMs), enabling communication between their respective latent spaces. To achieve the alignment, we propose two paradigms to support both open-source trainable LLMs and commercial frozen LLMs. We leverage this aligned architecture to develop the first generative foundation model for netlists, unleashing LLMs’ generative reasoning capability on the low-level and bit-blasted netlists. GenEDA enables three unprecedented generative netlist functional reasoning tasks, where it reversely generates high-level functionalities such as specifications and RTL code from low-level netlists. These tasks move beyond traditional gate function classification to direct generation of full-circuit functionality. Experiments demonstrate that GenEDA significantly boosts advanced LLMs’ (e.g., GPT and DeepSeek series) performance in all tasks. Wenji Fang, Wang Jing, Yao Lu 0031, Shang Liu 0006, Zhiyao Xie |
ICCAD | 1 |
| 2025 | CircuitFusion: Multimodal Circuit Representation Learning for Agile Chip DesignabstractThe rapid advancements of AI rely on the support of integrated circuits (ICs). However, the growing complexity of digital ICs makes the traditional IC design process costly and time-consuming. In recent years, AI-assisted IC design methods have demonstrated great potential, but most methods are task-specific or focus solely on the circuit structure in graph format, overlooking other circuit modalities with rich functional information. In this paper, we introduce CircuitFusion, the first multimodal and implementation-aware circuit encoder. It encodes circuits into general representations that support different downstream circuit design tasks. To learn from circuits, we propose to fuse three circuit modalities: hardware code, structural graph, and functionality summary. More importantly, we identify four unique properties of circuits: parallel execution, functional equivalent transformation, multiple design stages, and circuit reusability. Based on these properties, we propose new strategies for both the development and application of CircuitFusion: 1) During circuit preprocessing, utilizing the parallel nature of circuits, we split each circuit into multiple sub-circuits based on sequential-element boundaries, each sub-circuit in three modalities. It enables fine-grained encoding at the sub-circuit level. 2) During CircuitFusion pre-training, we introduce three self-supervised tasks that utilize equivalent transformations both within and across modalities. We further utilize the multi-stage property of circuits to align representation with ultimate circuit implementation. 3) When applying CircuitFusion to downstream tasks, we propose a new retrieval-augmented inference method, which retrieves similar known circuits as a reference for predictions. It improves fine-tuning performance and even enables zero-shot inference. Evaluated on five different circuit design tasks, CircuitFusion consistently outperforms the state-of-the-art supervised method specifically developed for every single task, demonstrating its generalizability and ability to learn circuits' inherent properties. Wenji Fang, Zhiyao Xie |
ICLR | 1 |
| 2025 | Profile-Guided Temporal PrefetchingabstractTemporal prefetching shows promise for handling irregular memory access patterns, which are common in data-dependent and pointer-based data structures.Recent studies introduced on-chip metadata storage to reduce the memory traffic caused by accessing metadata from off-chip DRAM.However, existing prefetching schemes struggle to efficiently utilize the limited on-chip storage.An alternative solution, software indirect access prefetching, remains ineffective for optimizing temporal prefetching.In this work, we propose Prophet-a hardware-software codesigned framework that leverages profile-guided methods to optimize metadata storage management.Prophet profiles programs using counters instead of traces, injects hints into programs to guide metadata storage management, and dynamically tunes these hints to enable the optimized binary to adapt to different program inputs.Prophet is designed to coexist with existing hardware temporal prefetchers, delivering efficient, high-performance solutions for frequently executed workloads while preserving the original runtime scheme for less frequently executed workloads.Prophet outperforms the state-of-the-art temporal prefetcher, Triangel, by 14.23%, effectively addressing complex temporal patterns where prior profile-guided solutions fall short (only achieving 0.1% performance gain).Prophet delivers superior performance across all evaluated workload inputs, introducing negligible profiling, analysis, and instruction overhead. Mengming Li, Qijun Zhang, Yichuan Gao, Wenji Fang, Yao Lu 0031, Yongqing Ren, Zhiyao Xie |
ISCA | 4 |
| 2025 | Transferable Presynthesis PPA Estimation for RTL Designs With Data Augmentation TechniquesabstractIn modern VLSI design flow, evaluating the quality of register-transfer level (RTL) designs involves time-consuming logic synthesis using electronic design automation tools, a process that often slows down early optimization. While recent machine learning (ML) solutions offer some advancements, they typically struggle with maintaining high accuracy across any given RTL design. In this work, we propose an innovative transferable presynthesis power, performance, and area (PPA) estimation framework named MasterRTL. It first converts the hardware description language code to a new bit-level design representation named the simple operator graph (SOG). By only adopting single-bit simple operators, this SOG proves to be a general representation that unifies different design types and styles. The SOG is also more similar to the target gate-level netlist, reducing the gap between the RTL representation and netlist. In addition to the new SOG representation, MasterRTL proposes new ML methods for the RTL-stage modeling of timing, power, and area separately. Compared with the state-of-the-art solutions, the experiment on a comprehensive dataset with 90 different designs shows accuracy improvement by 0.33, 0.22, and 0.15 in correlation for total negative slack (TNS), worst negative slack (WNS), and power, respectively. Besides the prediction of the synthesis results, MasterRTL also excels in accurately predicting layout-stage PPA based on the RTL designs and in adapting across different technology nodes and process corners. Furthermore, we investigate two effective data augmentation techniques: 1) a graph generation method and 2) a large language model (LLM)-based approach. Our results validate the effectiveness of the generated RTL designs in mitigating the data shortage challenges. Wenji Fang, Yao Lu 0031, Shang Liu 0006, Qijun Zhang, Ceyu Xu, Lisa Wu Wills, Hongce Zhang, Zhiyao Xie |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 1 |
| 2025 | RTLCoder: Fully Open-Source and Efficient LLM-Assisted RTL Code Generation TechniqueabstractThe automatic generation of RTL code (e.g., Verilog) using natural language instructions and large language models (LLMs) has attracted significant research interest recently. However, most existing approaches heavily rely on commercial LLMs, such as ChatGPT, while open-source LLMs tailored for this specific design generation task exhibit notably inferior performance. The absence of high-quality open-source solutions restricts the flexibility and data privacy of this emerging technique. In this study, we present a new customized LLM solution with a modest parameter count of only 7B, achieving better performance than GPT-3.5 on all representative benchmarks for RTL code generation. Especially, it outperforms GPT-4 in VerilogEval Machine benchmark. This remarkable balance between accuracy and efficiency is made possible by leveraging our new RTL code dataset and a customized LLM algorithm, both of which have been made fully open-source. Furthermore, we have successfully quantized our LLM to 4-bit with a total size of 4 GB, enabling it to function on a single laptop with only slight performance degradation. This efficiency allows the RTL generator to serve as a local assistant for engineers, ensuring all design privacy concerns are addressed. Shang Liu 0006, Wenji Fang, Yao Lu 0031, Jing Wang 0171, Qijun Zhang, Hongce Zhang, Zhiyao Xie |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 2 |
| 2024 | Annotating Slack Directly on Your Verilog: Fine-Grained RTL Timing Evaluation for Early OptimizationabstractIn digital IC design, compared with post-synthesis netlists or layouts, the early register-transfer level (RTL) stage offers greater optimization flexibility for both designers and EDA tools. However, timing information is typically unavailable at this early stage. Some recent machine learning (ML) solutions propose to predict the total negative slack (TNS) and worst negative slack (WNS) of an entire design at the RTL stage, but the fine-grained timing information of individual registers remains unavailable. In this work, we address the unique challenges of RTL timing prediction and introduce our solution named RTL-Timer. To the best of our knowledge, this is the first fine-grained general timing estimator applicable to any given design. RTL-Timer explores multiple promising RTL representations and proposes customized loss functions to capture the maximum arrival time at register endpoints. RTL-Timer's finegrained predictions are further applied to guide optimization in a standard synthesis flow. The average results on unknown test designs demonstrate a correlation above 0.89, contributing around 3% WNS and 10% TNS improvement after optimization. Wenji Fang, Shang Liu 0006, Hongce Zhang, Zhiyao Xie |
DAC | 1 |
| 2024 | OpenLLM-RTL: Open Dataset and Benchmark for LLM-Aided Design RTL GenerationabstractThe automated generation of design RTL based on large language model (LLM) and natural language instructions has demonstrated great potential in agile circuit design. However, the lack of datasets and benchmarks in the public domain prevents the development and fair evaluation of LLM solutions. This paper highlights our latest advances in open datasets and benchmarks from three perspectives: (1) RTLLM 2.0, an updated benchmark assessing LLM’s capability in design RTL generation. The benchmark is augmented to 50 hand-crafted designs. Each design provides the design description, test cases, and a correct RTL code. (2) AssertEval, an open-source benchmark assessing the LLM’s assertion generation capabilities for RTL verification. The benchmark includes 18 designs, each providing specification, signal definition, and correct RTL code. (3) RTLCoder-Data, an extended open-source dataset with 80K instruction-code data samples. Moreover, we propose a new verification-based method to verify the functionality correctness of training data samples. Based on this technique, we further release a dataset with 7K verified high-quality samples. These three studies are integrated into one framework, providing off-the-shelf support for the development and evaluation of LLMs for RTL code generation and verification. Finally, extensive experiments indicate that LLM performance can be boosted by enlarging the training dataset, improving data quality, and improving the training scheme. Shang Liu 0006, Yao Lu 0031, Wenji Fang, Mengming Li, Zhiyao Xie |
ICCAD | 3 |
| 2024 | Large circuit models: opportunities and challengesabstractAbstract Within the electronic design automation (EDA) domain, artificial intelligence (AI)-driven solutions have emerged as formidable tools, yet they typically augment rather than redefine existing methodologies. These solutions often repurpose deep learning models from other domains, such as vision, text, and graph analytics, applying them to circuit design without tailoring to the unique complexities of electronic circuits. Such an “AI4EDA” approach falls short of achieving a holistic design synthesis and understanding, overlooking the intricate interplay of electrical, logical, and physical facets of circuit data. This study argues for a paradigm shift from AI4EDA towards AI-rooted EDA from the ground up, integrating AI at the core of the design process. Pivotal to this vision is the development of a multimodal circuit representation learning technique, poised to provide a comprehensive understanding by harmonizing and extracting insights from varied data sources, such as functional specifications, register-transfer level (RTL) designs, circuit netlists, and physical layouts. We champion the creation of large circuit models (LCMs) that are inherently multimodal, crafted to decode and express the rich semantics and structures of circuit data, thus fostering more resilient, efficient, and inventive design methodologies. Embracing this AI-rooted philosophy, we foresee a trajectory that transcends the current innovation plateau in EDA, igniting a profound “shift-left” in electronic design methodology. The envisioned advancements herald not just an evolution of existing EDA tools but a revolution, giving rise to novel instruments of design-tools that promise to radically enhance design productivity and inaugurate a new epoch where the optimization of circuit performance, power, and area (PPA) is achieved not incrementally, but through leaps that redefine the benchmarks of electronic systems’ capabilities. Zhufei Chu, Wenji Fang, Tsung-Yi Ho, Ru Huang 0001, Yu Huang 0005, Sadaf Khan, Yun Liang 0001, Yibo Lin, Guojie Luo, Hongyang Pan, Zhengyuan Shi, Guangyu Sun 0003, Dimitrios Tsaras, Runsheng Wang, Ziyi Wang 0010, Xinming Wei, Zhiyao Xie, Qiang Xu 0001, Chenhao Xue, Junchi Yan, Bei Yu 0001, Mingxuan Yuan, Evangeline F. Y. Young, Xuan Zeng 0001, Haoyi Zhang, Zuodong Zhang, Hui-Ling Zhen, Binwu Zhu, Keren Zhu 0001, Sunan Zou |
Sci. China Inf. Sci. | 4 |
| 2024 | Erratum to: Large circuit models: opportunities and challenges
Zhufei Chu, Wenji Fang, Tsung-Yi Ho, Ru Huang 0001, Yu Huang 0005, Sadaf Khan, Yun Liang 0001, Yibo Lin, Guojie Luo, Hongyang Pan, Zhengyuan Shi, Guangyu Sun 0003, Dimitrios Tsaras, Runsheng Wang, Ziyi Wang 0010, Xinming Wei, Zhiyao Xie, Qiang Xu 0001, Chenhao Xue, Junchi Yan, Bei Yu 0001, Mingxuan Yuan, Evangeline F. Y. Young, Xuan Zeng 0001, Haoyi Zhang, Zuodong Zhang, Hui-Ling Zhen, Binwu Zhu, Keren Zhu 0001, Sunan Zou |
Sci. China Inf. Sci. | 4 |
| 2024 | TTNN: A Physically Guided Deep Learning Model for Focal Depth and Epicenter Distance Estimation Based on Multistation WaveformsabstractEarthquake localization is an important part of the seismicity monitoring workflow and catalog building, and it plays a fundamental role in earthquake research. The accurate estimation of the focal depth and epicenter distance is a crucial step in earthquake localization. Recent developments in deep learning seismology have shown promising results in tackling the issues related to time-consuming and low automation procedures in earthquake location estimation workflows. However, it is crucial to acknowledge that recent purely data-driven machine learning methods have some limitations, such as overfitting and insufficient generalization performance. To this end, a physically guided deep learning model, named travel time neural network (TTNN), is proposed for estimating the focal depth and epicenter distance using records collected from four stations. The TTNN is trained by 43868 three-component seismic records from 10967 earthquakes in Southern California. Incorporating the travel time equations of the P and S waves into the loss function enhances the interpretability and robustness of TTNN and also leads to a slight improvement in estimation performance. As a result, the network achieves a mean absolute error (MAE) of 1.81 km for focal depth, 1.46 km for epicenter distance, and 3.98 km for epicenter location on the testing set. The TTNN exhibits superior performance compared to the existing deep learning methods, indicating its potential as a powerful tool for rapid and accurate estimation of earthquake location. The source code is available athttps://github.com/duofaji/TTNN. Duofa Ji, Wenji Fang, Changhai Zhai, Zelin Cao, Yuhong Ma |
IEEE Trans. Geosci. Remote. Sens. | 2 |
| 2023 | MasterRTL: A Pre-Synthesis PPA Estimation Framework for Any RTL DesignabstractIn modern VLSI design flow, the register-transfer level (RTL) stage is a critical point, where designers define precise design behavior with hardware description languages (HDLs) like Verilog. Since the RTL design is in the format of HDL code, the standard way to evaluate its quality requires time-consuming subsequent synthesis steps with EDA tools. This time-consuming process significantly impedes design optimization at the early RTL stage. Despite the emergence of some recent ML-based solutions, they fail to maintain high accuracy for any given RTL design. In this work, we propose an innovative pre-synthesis PPA estimation framework named MasterRTL. It first converts the HDL code to a new bit-level design representation named the simple operator graph (SOG). By only adopting single-bit simple operators, this SOG proves to be a general representation that unifies different design types and styles. The SOG is also more similar to the target gate-level netlist, reducing the gap between RTL representation and netlist. In addition to the new SOG representation, MasterRTL proposes new ML methods for the RTL-stage modeling of timing, power, and area separately. Compared with state-of-the-art solutions, the experiment on a comprehensive dataset with 90 different designs shows accuracy improvement by 0.33, 0.22, and 0.15 in correlation for total negative slack (TNS), worst negative slack (WNS), and power, respectively. Wenji Fang, Yao Lu 0031, Shang Liu 0006, Qijun Zhang, Ceyu Xu, Lisa Wu Wills, Hongce Zhang, Zhiyao Xie |
ICCAD | 1 |
| 2023 | WASIM: A Word-level Abstract Symbolic Simulation Framework for Hardware Formal VerificationabstractAbstract This paper demonstrates the design and usage of WASIM, a word-level abstract symbolic simulation framework with pluggable abstraction/refinement functions. WASIM is useful in the formal verification of functional properties on register-transfer level (RTL) hardware designs. Users can control the symbolic simulation process and tune the level of abstraction by interacting with WASIM through its Python API. WASIM can be used to directly check formal properties on symbolic traces or to extract useful fragments from symbolic representations to construct safe inductive invariants as a correctness certificate. We demonstrate the utility of WASIM on the verification of two pipelined hardware designs. WASIM and the case studies are available under open-source license at: [9]. Wenji Fang, Hongce Zhang |
TACAS (2) | 1 |
| 2023 | r-map: Relating Implementation and Specification in Hardware Refinement CheckingabstractRefinement checking is an important formal verification method that checks if a hardware implementation complies with (in other words, refines) a given specification. It has been widely used in processor and nonprocessor verification. In refinement checking, a refinement mapping is needed to relate the implementation and the specification. Despite the wide adoption of refinement checking, there is currently no general format or standard for the mapping—most prior works employed a certain property specification language (e.g., the SystemVerilog assertion) to write ad-hoc properties that describe the mapping relation. These manually written properties are usually not well structured and are often difficult to design or understand. In this article, we present${\tt r{-}map}$, a language for refinement mapping.${\tt r{-}map}$relates the implementation and the specification in a more concise and comprehensible way. We evaluate${\tt r{-}map}$in the refinement checking of practical hardware designs. In our case study,${\tt r{-}map}$shows a significant reduction of human efforts compared to manually writing refinement properties. We also show how${\tt r{-}map}$can help to scale up formal verification. Wenji Fang, Guangyu Hu, Hongce Zhang |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 1 |