Claire Wolf

Project IceStorm provides the first end-to-end open source FPGA toolchain, was originally presented at 32c3, and only targetted Lattice iCE40 FPGAs. nextpnr is the next big step for open source FPGA tools, providing a retargetable open source FPGA place-and-route tool that will enable open source flows for many different FPGAs from many different vendors.

nextpnr is a retargetable FOSS FPGA place-and-route tool that is replacing arachne-pnr as place-and-route tool in the IceStorm open source iCE40 flow. (I have originally presented IceStorm and arachne-pnr at 32c3.) nextpnr is retargetable, meaning it can be ported to other FPGA architectures easily, uses timing-driven algorithms, provides a python scripting API, supports complex placement and floorplanning constraints, and has a nice GUI. Python and GUI support are optional, which may be useful when deploying nextpnr on an embedded platform. In short: It is a big step forward for open source FPGA tools, attempting to close the gap to vendor tools in some aspects, and even setting new standards in other aspects. As of now, iCE40 FPGAs (Project IceStorm) and ECP5 FPGAs (Project Trellis) are supported in nextpnr, but support for more architectures is expected to follow in short order.

Formal hardware verification (hardware model checking) can prove that a design has a specified property. Historically only very simple properties in simple designs have been provable this way, but improvements in model checkers over the last decade enable us to prove very complex design properties nowadays. riscv-formal is a framework for formally verifying RISC-V processors directly against a formal ISA specification. In this presentation I will discuss how the complex task of verifying a processor against the ISA specification is broken down into smaller verification problems, and other techniques that I employed to successfully implement riscv-formal.

Formal hardware verification (hardware model checking) can prove that a design has a specified property. This is different from simulation, which can only demonstrate that a property holds for some concrete traces (sets of inputs). Historically only very simple properties in simple designs have been provable this way, but improvements in model checkers over the last decade enable us to prove very complex design properties nowadays. riscv-formal is a framework for formally verifying RISC-V processors directly against a formal ISA specification. (The ISA specification used in riscv-formal is itself formally verified against Spike , the official RISC-V simulator and "golden reference" implementation.) riscv-formal can be made to work with any existing processor design, all that is needed is to add an additional RVFI (RISC-V formal interface) trace port to the core. riscv-formal by default uses the open source SymbiYosys toolchain to perform the formal proofs, but it should be compatible with all major HDL formal verification flows. In this presentation I will discuss how the complex task of verifying a processor against the ISA specification is broken down into smaller verification problems in riscv-formal, how to implement RVFI, how integrate a core with riscv-formal, and what kind of bugs can be detected using our method. Most of the proofs performed by riscv-formal are bounded proofs, i.e. it is only proven that the properties hold for the first N cycles after reset. But with a sufficiently large N we can create high confidence that in fact all relevant states can be reached within the bound of the proof and that therefore the bounded case is a sufficient proxy for the more general unbounded case. Abstractions, cut-points, and blackboxing can further help extend the effective bound of the proof. The presentation also touches on those techniques.

Yosys (Yosys Open Synthesis Suite) is an Open Source Verilog synthesis and verification tool.

Project IceStorm aims at reverse engineering and documenting the bit-stream format of Lattice iCE40 FPGAs and providing simple tools for analyzing and creating bit-stream files, including a tool that converts iCE40 bit-stream files into behavioral Verilog. Currently the bitstream format for iCE40 HX1K and HX8K is fully documented and supported by the tools.

Arachne-PNR is an Open Source place&route tool for iCE40 FPGAs based on the databases provided by Project IceStorm. It converts BLIF files into an ASCII file format that can be turned into a bit-stream by IceStorm tools.

This three projects together implement a complete open source tool-chain for iCE40 FPGAs. It is available now and it is feature complete (with the exception of timing analysis, which is work in progress).