Versatile Hardware Analysis Techniques - From Waveform-based Analysis to Formal Verification
Sprache des Vortragstitels:
Englisch
Original Tagungtitel:
Forum on Design Languages (FDL)
Sprache des Tagungstitel:
Englisch
Original Kurzfassung:
With the slowing-down of Moore?s law, the industry is scrambling to keep up with the still growing demand for powerful hardware designs. One strategy to cope with these demands is the move to increasingly application-specific designs, of which AI accelerators are a prime example. Another example of this move to application-specific designs is the emergence of the RISC-V Instruction Set Architecture (ISA). It is not only royalty-free, but also highly modular, thus leading to an extensive offering of RISC-V processors covering all application domains from embedded to high-performance computing. Naturally, design complexities and design sizes are still growing rapidly, thus taken together, creating many new challenges for Electronic Design Automation (EDA) toolchains, especially for the labor-intensive verification and debugging phases. This thesis proposes several versatile hardware analysis techniques that tackle existing and new challenges. These techniques cover different phases of the hardware development process, including the verification, debugging, and post-synthesis optimization phases. The first contribution is a novel processor verification methodology based on a new application of equivalence checking. The second contribution is a framework for formally verifying microcode. The third contribution is the Waveform Analysis Language (WAL), a Domain Specific Language (DSL) for analyzing waveforms. We evaluate WAL in multiple case studies, including analyzing processor performance metrics for various RISC-V processors and the integration of WAL into a Hardware Description Language (HDL) in the form of analysis passes. The fourth and final contribution is a netlist optimization methodology based on external constraints. All contributions and their effectiveness are presented in detail and are evaluated in extensive experiments and case studies. Furthermore, all contributions are fully implemented and made available as open-source software.
Forschungs-