Erfolgreiche Verteidigung der Dissertation
Dr. Lennart Weingarten
Dr. Lennart Weingarten hat seine Dissertation "Efficient Formal Verification of Complex Designs" erfolgreich verteidigt.
This thesis addresses the challenge of efficient formal hardware verification. Even in the era beyond Moore’s Law, where the scaling of transistor density has slowed, architectural complexity continues to increase. Ensuring the correctness of increasingly large and complex designs, such as processors, is not only a challenge but also a bottleneck in the Electronic Design Automation (EDA) development flow. As a time-consuming step, making formal verification efficient is essential. The work focuses on the formal verification of RISC-V processor designs and the fundamental building blocks of neuromorphic processors, such as Multiply-Accumulate (MAC) and Dot-Product (DP) units.
For the verification of single- and multi-cycle RISC-V designs, a process was developed that allows for the efficient functional verification of the RV32I base instructions using Binary Decision Diagrams (BDDs). The efficiency of this verification flow stems from the BDD data structure itself, as well as the generation of BDDs using the ITE (If-Then-Else) operator, which allows for polynomially bounded generation and, therefore, bounded verification. Beyond the RV32I, multiplication instructions from the RISC-V M-extension were verified using an extended process that integrates Symbolic Computer Algebra (SCA).
The second part of this work consists of several contributions. First, an initial feasibility study for MAC and DP units using SCA showed promising results and high scalability for simple designs. Second, a scalability analysis was conducted under design constraints such as area and delay optimization. To predict the likelihood of verifiability, scalability indicators were developed to determine if a design with a small bit-width remains verifiable when scaled to larger sizes. Beyond structurally simple designs, optimized behavioral designs were also considered. For these, new techniques such as transformation-aided verification were developed, showing promising results in mitigating intermediate term explosion in SCA-based verification. Finally, an initial upper-bound proof derived from And-Inverter Graph (AIG) rules is presented. A corresponding case study for carry-ripple adders demonstrates the impact of traversal ordering and the effectiveness of graph splitting to verify primary outputs in isolation.
Overall, the work establishes theoretical and experimental bounds for BDD-based RISC-V processor verification and introduces scalable algebraic techniques to mitigate complexity in SCA-based verification for neuromorphic processor components. By bridging these two domains, the thesis provides a robust framework that ensures formal verification remains efficient and predictable even as architectural complexity grows.
In X teilen
In LinkedIn teilen
