Formal Verification of WARP-V, a TL-Verilog RISC-V Core Generator

on YouTube ↗18m

" summary

Describes WARP-V, a TL-Verilog CPU core generator that can produce RISC‑V and custom-ISA designs from simple microcontrollers up to seven-stage pipelined cores, and explains how TL‑Verilog’s timing-abstraction and transaction-level design are used both for design and for verification. Shows how WARP‑V was formally verified with riscv-formal (Clifford Wolf’s RISC‑V formal framework) and reports that all RISC‑V configurations were verified with a single page of verification code.

AI-written summary · about

" chapters (9)

1. 0:00Start
2. 1:23TL-Verilog Teaser
3. 4:24Makerchip
4. 4:53WARP-V Goal: Flexibility
5. 5:34Approach
6. 7:056-Stage WARP-V
7. 9:22Let's put it into perspective
8. 10:52Wrap it up!
9. 16:45Code Size Comparison

" related talks

• 16mIntroduction to RISC-V Processor VerificationLarry Lapides · embedded world 2023
• 13mIntroduction to RISC-V Processor VerificationLarry Lapides · embedded world 2022
• 21mThe New Verification Ecosystem that Supports RISC-V Verification fo...Lee Moore, John Sotiropoulos · RISC-V Summit 2022
• 17mDemo: RISC-V Models for Verification, Software Development and Architectural Explor...Larry Lapides · RISC-V Summit 2022
• 21mA Comparative Analysis of RISC-V Architecture Based on the RISC-V SoC DV ExperienceMoonki Jang · RISC-V Summit North America 2023
• 18mIntroducing Scalable New Core IP for Mission Critical UseAniket Saha, Murali Vijayaraghavan · RISC-V Summit 2019
• 11mFast Virtual Platforms for Custom RISC-V ProcessorsZdenek Prikryl, Lukas Jünger · RISC-V at embedded world 2024
• 09mExploring RISC-V architectures with VPSim, a virtual prototyping environmentLilia Zaourar · RISC-V Summit Europe 2024