TY - GEN
T1 - Parameterized Design and Formal Verification of Multi-ported Memory
AU - Xiang, Mufan
AU - Li, Yongjian
AU - Tan, Sijun
AU - Zhao, Yongxin
AU - Chi, Yiwei
N1 - Publisher Copyright:
© 2022 IEEE.
PY - 2022
Y1 - 2022
N2 - 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.
AB - 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.
KW - Chisel
KW - Hardware Formal Verification
KW - Multi-ported Memory
KW - Parameterized Design
UR - https://www.scopus.com/pages/publications/85130089891
U2 - 10.1109/ICECCS54210.2022.00013
DO - 10.1109/ICECCS54210.2022.00013
M3 - 会议稿件
AN - SCOPUS:85130089891
T3 - Proceedings of the IEEE International Conference on Engineering of Complex Computer Systems, ICECCS
SP - 33
EP - 41
BT - Proceedings - 2022 26th International Conference on Engineering of Complex Computer Systems, ICECCS 2022
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - 26th International Conference on Engineering of Complex Computer Systems, ICECCS 2022
Y2 - 26 March 2022 through 30 March 2022
ER -