r-map: Relating Implementation and Specification in Hardware Refinement Checking
Refinement 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 r−map , a language for refinement mapping. r−map relates the implementation and the specification in a more concise and comprehensible way. We evaluate r−map in the refinement checking of practical hardware designs. In our case study, r−map shows a significant reduction of human efforts compared to manually writing refinement properties. We also show how r−map can help to scale up formal verification.
Hi! I’m Wenji Fang (方闻绩), a Ph.D. candidate at the Electronic and Computer Engineering Department of the Hong Kong University of Science and Technology, advised by Prof. Zhiyao Xie. Previously, I received my M.Phil in microelectronics from the Hong Kong University of Science and Technology (Guangzhou), advised by Prof. Hongce Zhang & Prof. Zhiyao Xie, and my B.Eng in electrical engineering from Nanjing University of Aeronautics and Astronautics.
My research focuses on AI for Electronic Design Automation (EDA), with the goal of advancing AI-driven paradigms for VLSI design and verification. I have published 10+ first-author papers in leading EDA and AI venues, including DAC, ICCAD, ASP-DAC, TCAD, and ICLR.
I received the inaugural LLM-Aided Design Fellowship and the 2nd Place Award in the ACM SIGDA Student Research Competition. Beyond academia, I have gained industry experience through my internship at NVIDIA Research and Peng Cheng Laboratory.