Formally Verifying WARP-V, an Open-Source TL-Verilog RISC-V Core Generator

Steven Hoover, Ákos Hadnagy

Timing-abstract and transaction-level design using TL-Verilog have shown significant productivity gains for logic design. In this work, we explored the natural extension of transac…