r-map: Relating Implementation and Specification in Hardware Refinement Checking

Abstract

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 non-processor 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.

Guangyu (Gary) Hu

Researcher at Huawei Hong Kong Research Center, Fermat Lab

My research interests include LLM + formal verification reasoning and hardware formal verification.