A Methodology for Verifying Memory Access Protocols in Behavioral Synthesis

Abstract — Memory is one of the most important components to be optimized in the several phases of the synthesis process. construct which hides the detail implementations of the mem-ory. Consequently, for a vendor’s memory, behavioral syn-thesis should create a clean model of the memory wrapper which abstracts the properties of the memory that are re-quired to interface to the rest of the circuit. However, this wrapping process invariably demands the verification prob-lem of the memory access protocols in order to be safely used in behavioral synthesis environment. In this paper, we pro-pose a systematic methodology of verifying the correctness of the memory wrapper. Specifically, we analyze the com-plexity of the problem, and derive an effective solution which is not only practically efficient but also highly reliable. For designers who use memories as design components in behav-ioral synthesis, automating our solution shortens the verifica-tion time significantly in contrast of simulating memory ac-cesses in the context of full design, which is a quite complex and time-consuming process, especially for designs with many memory access operations.