Formal Based Methodology for Inferring Memory Mapped Registers
Haytham Saafan, Mohamed Watheq El-Kharashi, Ashraf Salem · 2016
System on Chip modules are usually controlled and configured through memory mapped registers. Those are special registers written and read through bus interfaces by execution of write and read operations associated with specific address values, like writing to and reading from memories. Verification of the behavior of such registers is challenging because of their big quantities on the System on Chip and the variety of modes of their operation. Recently Formal verification is proven a better and a faster methodology for verifying the access policies of the memory mapped register compared to traditional simulation pseudo random techniques. The industry-wide available formal based checkers for register access verification require knowledge of the hardware physical name of the register which is not usually available with the register specification documents. This paper shows an automated approached based on both structural and formal analysis of the design under test to induce the hardware names of the memory mapped registers. Results of successfully applying the presented methodology on three open cores are provided.