vmurali
commented
5 years ago Thanks for the suggestion. There are plans to use FIRRTL as the backend, since, obviously SiFive relies on Chisel/FIRRTL a lot :)
However, there is one important issue that's making using FIRRTL non-obvious. Notice that there's a CompileVerifiable.v file, which is a formally proven compiler that converts Kami programs into an RTL representation in Coq (called CompActionT in that file). This RTL representation can be pretty printed into any language (the pretty printer for the target of the verified compiler will be written shortly). The guarantee this verified compiler from Kami to (internal) RTL representation provides is that the RTL circuit generated after compiling the Kami program matches the semantics of the original Kami program. If, instead, FIRRTL was used and it performs optimizations on the RTL, then those optimizations are not guaranteed to be correct, potentially making the final circuit unverified.
Of course, the pretty printer of the internal RTL is also not guaranteed to be correct, as it can have bugs in pretty printing; but one has to draw the line somewhere.
In the formal verification circles, we call the stuff that has to be blindly trusted by the user as a trusted code base (TCB). In the current case, if an implementation has been verified using Kami against a specification, the TCB contains a) Kami's definition (i.e. whether Kami's semantics are a sound representation of some abstract hardware) b) Coq's type checking c) Coq's extraction mechanism and Kami's optimizations for extraction d) The specification of the hardware module (against which the implementation is verified) e) Pretty printer to Verilog.
If one adds FIRRTL to it, then the new TCB becomes a) Kami's definition (i.e. whether Kami's semantics are a sound representation of some abstract hardware) b) Coq's type checking c) Coq's extraction mechanism and Kami's optimizations for extraction d) The specification of the hardware module (against which the implementation is verified) e) Pretty printer to FIRRTL f) FIRRTL's optimization passes
So, that's one formal proof-based technical reason to not switch to FIRRTL yet.
There's one more mundane reason - FIRRTL does not support constructing clusters as expressions :) (i.e. one cannot build an array expression or a struct expression). This is a technical non-issue, but I am waiting for that to be available before I create a FIRRTL backend - some of the Chisel developers have been notified of this.
(Edited to include the specification of the hardware module against which the implementation is verified against in the TCB, and Coq's extraction mechanism)
As you obviously know FPGA and ASIC world suffers a lot from fragmentation - some tools produce Verilog, some VHDL, some - only subsets of them, creating low-level LLVM-like alternative will help everyone, so HDL implementations will opt only for generating this low-level HDL and routing/synthesizers accept it. This tool focuses on the producing Verilog, so it lacks the ability to work with VHDL-oriented toolchains. LLVM or WebAssembly - you can see how many languages and targets are supported now by both. With more open source tools for FPGA this is more feasible now than ever. Most of the people suggest to adapt FIRRTL for this. You can read more about FIRRTL on their site. Please check the discussion and provide a feedback if you have any. There is a good paper on FIRRTL design and its reusability across different tools and frameworks.
See SymbiFlow/ideas#19 for deeper discussion.
See also the NetlistDB project.