Parameterized Design and Formal Verification of Multi-ported Memory

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.