Design and Verification of AMBA Advanced Extensible Interface Memory Using Assertion Based Formal Checks

Abstract

One of the hardest aspects of chip design is frequently functional verification. A given model's correct adherence to the specification is checked through functional verification. Additionally, it ensures that the implementation follows the specification. Functional verification has emerged as one of the major design process bottlenecks as a result of the quick increase in design size and complexity. The Advanced eXtensible Interface is designed as a collection of interdependent systems, each of which has a limited number of configurations or states. Finite State Machines (FSMs) consist of states and their transitions. The primary goal of the FSM is to check the flow of transactions in Network on Chip (NoC)s, where each transaction entering and exiting a subsystem must be secure, reliable, and pass through all of the state machine's different stages. The assertion-based formal checks for the design were supported by state machines for read and write situations. Assertions are used to verify design principles or requirements and produce errors or warnings when they fail. The AMBA AXI protocol is designed using SystemVerilog, and formal checks in the form of System Verilog assertions are used to examine the internal signals that provide read-write transactions of the memory that serves as the slave for the network on chip. The ability of the memory to react to different signals provided by the master is examined using the various burst transactions in terms of Fixed, Increment (INCR), and Wrap transactions. In this work, an AXI memory module is designed and verified using UVM and simulated using both vaivado and questasim.