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

This paper introduces TL-V erilog and W ARP-V and then describes the formal verification of WARP-V using riscv-formal, a formal verification framework for RISC-V. Timing-abstraction and transaction-level design are showing significant benefits for hardware modeling, but this is the first demonstration of their benefits for verification modeling. As evidence of these benefits, the verification of all RISC-V configurations of WARP-V is accomplished in a single page of code.

Continue reading

Paper 5: Introduction to TL-Ver & Front-End Symposium

Steve Hoover is the founder of Redwood EDA. Steve holds a BS in electrical engineering from Rensselaer Polytechnic Institute and an MS in computer science from the University of Illinois. He has designed numerous components for high-performance server CPUs and network architectures for DEC, Compaq, and Intel. Students will learn Transaction-Level Verilog modelingtechniques to generate Verilog models in half the time using the makerchip.comfree online IDE. A new open-source RISC-V CPU development effort will be introduced that showcases flexible IP design practices.

Continue reading