1 citations · 2 across the 12 of their papers we have counts for
12 papers
Forbench: Symbolic Simulation Helps Make Your Testbench More Formal
Ziyi Yang, Wenbin Che, Ziyue Zheng +2
Simulation remains the dominant approach in pre-silicon verification due to its ease of deployment and intuitive workflow. However, as simulation only explores a limited subset of…
Inverter Redistribution through Self-Dual and Self-Anti-Dual Function Transformation
Jingren Wang, Guangyu Hu, Shiju Lin +1
And-Inverter Graph (AIG)-based logic synthesis has been a cornerstone of digital design automation for several decades. While numerous optimization techniques have been developed f…
AutoINV: Automated Invariant Generation Framework for Formal Verification on High-Level Synthesis Designs
Xiaofeng Zhou, Linfeng Du, Guangyu Hu +3
High-level synthesis (HLS) transforms an algorithmic description of hardware from a higher abstraction (e.g., C/C++) into a register-transfer level (RTL) design, offering reduced d…
A-IC3: Learning-Guided Adaptive Inductive Generalization for Hardware Model Checking
Xiaofeng Zhou, Guangyu Hu, Hongce Zhang +1
The IC3 algorithm represents the state-of-the-art (SOTA) hardware model checking technique, owing to its robust performance and scalability. A significant body of research has focu…
IC3-Evolve: Proof-/Witness-Gated Offline LLM-Driven Heuristic Evolution for IC3 Hardware Model Checking
Mingkai Miao, Guangyu Hu, Ziyi Yang +1
IC3, also known as property-directed reachability (PDR), is a commonly-used algorithm for hardware safety model checking. It checks if a state transition system complies with a giv…
AutoPDR: Circuit-Aware Solver Configuration Prediction for Hardware Model Checking
Guangyu Hu, Chen Chen, Xiaofeng Zhou +3
Property Directed Reachability (PDR) is a powerful algorithm for formal verification of hardware and software systems, but its performance is highly sensitive to parameter configur…
LeGend: A Data-Driven Framework for Lemma Generation in Hardware Model Checking
Mingkai Miao, Guangyu Hu, Wei Zhang +1
Property checking of RTL designs is a central task in formal verification. Among available engines, IC3/PDR is a widely used backbone whose performance critically depends on induct…
EvolveGen: Algorithmic Level Hardware Model Checking Benchmark Generation through Reinforcement Learning
Guangyu Hu, Xiaofeng Zhou, Wei Zhang +1
Progress in hardware model checking depends critically on high-quality benchmarks. However, the community faces a significant benchmark gap: existing suites are limited in number,…
BDD2Seq: Enabling Scalable Reversible-Circuit Synthesis via Graph-to-Sequence Learning
Mingkai Miao, Jianheng Tang, Guangyu Hu +1
Binary Decision Diagrams (BDDs) are instrumental in many electronic design automation (EDA) tasks thanks to their compact representation of Boolean functions. In BDD-based reversib…
FORWORD: Accelerating Formal Datapath Verification via Word-Level Sweeping
Ziyi Yang, Guangyu Hu, Xiaofeng Zhou +4
Modern circuit design process increasingly adopts high-level hardware construction languages and parameterized design methodologies to shorten development cycles and maintain high…
E-morphic: Scalable Equality Saturation for Structural Exploration in Logic Synthesis
Chen Chen, Guangyu HU, Cunxi Yu +2
In technology mapping, the quality of the final implementation heavily relies on the circuit structure after technology-independent optimization. Recent studies have introduced equ…
E-Syn: E-Graph Rewriting with Technology-Aware Cost Functions for Logic Synthesis
Chen Chen, Guangyu Hu, Dongsheng Zuo +3
Logic synthesis plays a crucial role in the digital design flow. It has a decisive influence on the final Quality of Results (QoR) of the circuit implementations. However, existing…