Modern digital hardware is becoming ever more complex. And agile development, an efficient idea in software development, has been introduced into hardware. Furthermore, as a new hardware construction language, Chisel helps to raise the level of hardware design abstraction with the support of object-oriented and functional programming. Chisel plays a crucial role in future hardware design and open-source hardware development. However, the formal verification for Chisel is still limited. In this paper, we propose ChiselFV, a formal verification framework that has supported detailed formal hardware property descriptions and integrated mature formal hardware verification flows based on SymbiYosys. It builds on top of Chisel and uses Scala to drive the verification process. Thus the framework can be seen as an extension of Chisel. ChiselFV makes it easy to verify hardware designs formally when implementing them in Chisel.

Multi-ported memories are essential modules to provide parallel access for high-performance parallel computation systems such as VLIW and vector processors, etc. However, the design of multi-ported memories are rather complex and error-prone, which usually causes the high implementation cost. Therefore, the designs and verification of multi-ported memories become challenging. In this paper, we firstly present a modular and parameterized approach based on Chisel to design and implement multi-ported memory concisely. Furthermore, to verify the correctness of the design, we formalize properties of multi-write-read operations of the memories by generalized symbolic trajectory assertion (GSTE) graphs and verified them by two kinds of approaches: SystemVerilog Assertions-based, and GSTE-based approaches. Our verification through SVA and STE/GSTE successfully finds an error caused by misusing one parameter in our high-level design.