WARP-V is an open-source CPU core generator written in TL-Verilog with support for RISC-V and MIPS I. It is a demonstration and exploration vehicle for the flexibility that is possible using the emerging "transaction-level design" methodology. It can implement a single-stage, low-power microcontroller or a mid-range 7-stage CPU. Even the instruction-set architectures (ISAs) is configurable. WARP-V is an evolving library of CPU components as well as various compositions of them. It is driven by a community interested in transforming the silicon industry through open-source hardware and revolutionary design methodology.
WARP-V includes CPU core logic only with no current support for virtual memory, caches, or IOs. RISC-V implementations are formally verified using open-source tools in continuous integration testing. They have been formally verified also by Axiomise.
We built a configurator, so you can quickly build a CPU to suit your needs!
- Steve Hoover, "Pipelining RISC-V", Udemy 2018, webinar
- Steve Hoover, "Overcoming RTL", DAC 2018: slides
- Akos Hadnagy, "Formal Verification of WARP-V", ORConf 2018 and VSDOpen 2018: slides, video, and paper
- Steve Hoover: "Verifying a RISC-V in 1 Page of Code!", Linkedin and SemiWiki
- A Google Drive for this and other open-source TL-Verilog projects including some WARP-V block diagrams
- A LibreCores WARP-V Gitter Room for public discussion
In a clean directory:
git clone https://github.com/stevehoover/warp-v.git
cd warp-v
./init- Adaptable CPU core implementations (core only, no virtual memory, caches, I/Os)
- Reconfigurable pipeline (1-7 stages)
- Customizable ISA, with implementations of RISC-V ISA (RV32I), MIPS I, and a simple string-based ISA for educational use
- RT-Level implementation detail
- A simple ~12-instruction test for each ISA
- For RISC-V ISA:
- An assembler for hard-coded test programs
- Formal verification in CI (continuous integration testing)
- Implementation characterized on AWS data-center FPGAs
- A small code base (single < 3K-line file (heavily-commented) implements all WARP-V variants, assembler, tests, formal verification harness, and Xilinx implementation)
As an exploration vehicle for capabilities that are not yet defined in the TL-Verilog language spec, WARP-V intentionally pushes the limits of code construction using an M4-based flow. While TL-Verilog documentation and tools are fairly mature, the M4 layer intended only for research.an undocumented proof-of-concept framework (even when old-school Verilog features might suffice). If you've come here to learn about TL-Verilog for RISC-V design, you'd be better served to study the cores developed in the Microprocessor for You in Thirty Hours Workshop.
WARP-V uses bleeding-edge modeling methodology that provides an unprecedented level of flexibility without sacrificing gate-level control. To understand WARP-V and how to utilize it, it helps to first gain an appreciation for this methodology, which involves two layers:
Transaction-Level Verilog extends Verilog/SystemVerilog with constructs for pipelines, transactions, etc. This provides a convenient modeling framework for parameterization at a higher level, but without sacrificing gate-level control. You can learn more about TL-Verilog at makerchip.com.
Code construction techniques for TL-Verilog are an active area of research. Before native implementation, code construction is being explored through the use of a macro preprocessor, M4 (plus a bit of Perl). Macro preprocessing is used in WARP-V to enable a single definition of the instruction set to be used to generate:
- decode logic
- result selection logic for the execution unit
- an assembler
Logic related to replay and register bypass is generated based on CPU pipeline configuration.
There are simple uses of M4 that are easy to follow, such as including library files, defining constants, and instantiating macros. M4 features are supported in the Makerchip IDE as a short-term solution with some nice features to help with these use models. But M4 use in WARP-V goes way beyond these scenarios, intentionally pushing the limits of code construction. A small amount of code does a lot, but it is very messy, undocumented, and extremely difficult to debug. So it is important to give careful consideration to your intended use of WARP-V.
You can learn more about the WARP-V design methodology in these slides, presented at the Design Automation Conference in June 2018. Below is a corresponding poster.
High-level parameters are defined toward the top of the WARP-V file. You can modify parameters and compile from the command line, but it is easier to follow compilation steps and debug problems using the IDE at makerchip.com as described below. There is no better guide for understanding parameters at this point than code comments.
Since M4 macro-preprocessing is not for the faint of heart, once you've got a CPU that's close to what you want, you can take the generated code as source and go from there. Ideally, that would mean using the TL-Verilog as source, since you still get a great deal of flexibility at that level, but if you are stuck in the past, you can start with the Verilog or SystemVerilog.
Constructing an ISA from scratch would require heavy use of M4 and could be a tall order at this point. Small variations of RISC-V, however, are more feasible by making small adjustments to parameterization.
For RISC-V development (even if you are developing your own RISC-V core without using WARP-V itself) this repository has some useful infrastructure. It supports formal verification using riscv-formal run in continuous integration testing. So, you always know if your core is compliant.
WARP-V is implemented on FPGAs in the cloud using the 1st CLaaS (custom logic as a service) framework. You can implement your own customized WARP-V on FPGAs in the cloud, too!
You can find help in the LibreCores WARP-V Gitter Chat Room. You might find commercial assistance there as well.
A few pointers for exploring WARP-V in Makerchip:
- Learn TL-Verilog and Makerchip first, following tutorials and other resources, at makerchip.com. there are several courses available for building your own RISC-V CPU similar to WARP-V, but less parameterized, available via the menus.
- This link will Open the latest WARP-V in Makerchip.
- Reverse-engineer the WARP-V design at the TL-Verilog level, not by reading WARP-V source code. Configure WARP-V at warp-v.org as you choose, compile, and explore the model in the "Nav-TLV" pane.
- You can then correlate this back to the source code by clicking Nav-TLV line numbers. This highlights the corresponding source code line.
Speak up on the LibreCores WARP-V Gitter Chat Room and we'll help you find an appropriate way you can help out.
Keep in mind that WARP-V is a horrible starting point for learning TL-Verilog because of its heavy use of M4. If you are interested in microarchitectural contributions, learn TL-Verilog first at makerchip.com.
With a clear understanding of where to tread, you can navigate WARP-V and contribute successfully. WARP-V is a library with plenty of room to grow to cover a more complete spectrum of CPU microarchitecture. Be aware, however, that working with CPU microarchitecture means walking in a minefield of patents. Work with the community to define your contributions.
Work in a fork and submit push requests that have passed continuous integration (CI) testing (below). Your work is much more likely to be accepted if it is aligned with the community and doesn't risk patent infringement.
WARP-V RISC-V implementations are verified using the riscv-formal open-source formal verification framework. Everything for formal verification is in the formal directory. See the README.md file there.
formal/Makefile uses SandPiper(TM) SaaS Edition -- SandPiper running in the cloud as a service. No local SandPiper installation is required (but if the SandPiper SaaS service goes down, the build will fail).
(For other ISAs, Upscale might be a good direction for future work.)
RISC-V WARP-V cores have also been formally verified by Axiomise with some issues outstanding.
Travis-CI is used for continuous integration testing: WARP-V Travis CI. CI runs formal verification tests.
CI uses the formal/make_env.sh script to built the necessary tools from source. The result of this build is cached between builds (per branch) using a caching feature of Travis-CI. Caching is applied blindly, without regard to the availability of newer sources. CI scripts will check the latest sources against the ones from the cache and report differences near the end of the log. The cache can be cleared manually from the build page. Look under "More options" (upper-right).
Debugging Travis-CI failures can be awkward. To simplify things, if a formal check fails, CI scripts attempt to upload the failure traces using https://transfer.sh/. Look for messages near the end of the log file containing links to the uploaded traces for download and debug.
TODO: Add implementation data here.
We utilized the pipeline flexibility of TL-Verilog and WARP-V's pipeline parameterization to experiment with Vivado's ability to retime logic optimally. This showed that it is not necessary to precisely partition the CPU pipeline logic among pipeline stages in order to get good quality results. However, when tools must retime logic, runtime can be significantly impacted. Here is more detail.