Article-Journal

In modern VLSI design flow, evaluating the quality of register-transfer level (RTL) designs involves time-consuming logic synthesis using EDA tools, a process that often slows down early optimization. While recent machine learning solutions offer some advancements, they typically struggle with maintaining high accuracy across any given RTL design. In this work, we propose an innovative transferable 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, Master-RTL proposes new ML methods for the RTL-stage modeling of timing, power, and area separately. Compared with state-of-theart 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 synthesis results, MasterRTL also excels in accurately predicting layout-stage PPA based on RTL designs and in adapting across different technology nodes and process corners. Furthermore, we investigate two effective data augmentation techniques: a graph generation method and a Large Language Model (LLM)-based approach. Our results validate the effectiveness of the generated RTL designs in mitigating data shortage challenges.

Jul 1, 2024

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.

Jun 1, 2023

Lorem ipsum dolor sit amet, consectetur adipiscing elit. Duis posuere tellus ac convallis placerat. Proin tincidunt magna sed ex sollicitudin condimentum.

Sep 1, 2015