A methodology for verifying memory access protocols in behavioral synthesis

Memory is one of the most important components to be optimized in the several phases of the synthesis process. In behavioral synthesis, a memory is viewed as an abstract construct which hides the detail implementations of the memory. Consequently, for a vendor´s memory, behavioral synthesis should create a clean model of the memory wrapper which abstracts the properties of the memory that are required to interface to the rest of the circuit. However, this wrapping process invariably demands the verification problem of the memory access protocols in order to be safely used in behavioral synthesis environment. In this paper, we propose a systematic methodology of verifying the correctness of the memory wrapper. Specifically, we analyze the complexity 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 behavioral synthesis, automating our solution shortens the verification time significantly in contrast of simulating memory accesses in the context of full design, which is a quite complex and time-consuming process, especially for designs with many memory access operations.