Presentation
Breaking Sequential Depth Barriers: An FSM-Driven Bridge for the Formal Verification of Virtually Address-Mapped Hardware Registers
DescriptionThis paper presents the formal verification of a subsystem with indirect read mechanisms and a nonstandard access protocol. Verifying registers using the control and status register (CSR) protocol typically requires a proof accelerator to convert a standard bus into the CSR protocol. However, this secure design uses a custom protocol, creating unique formal verification challenges. In this design, writing to an IP register through the subsystem is straightforward and followed by polling a status register to check the write data status. The read data is available at a different address within the subsystem register map.
To address this, a protocol-to-protocol AMBA bridge is developed. The bridge converts write commands from the verification intellectual property (VIP) into writes for the device under test (DUT) and reads data from the DUT, returning it to the corresponding VIP address. Because the DUT does not return data at the same address, address conversion logic with several finite state machines (FSMs) is implemented. This approach allows the VIP to perform checks as expected, despite the indirect read mechanism.
Counter value abstraction is used to manage delays and simplify verification, ensuring efficient completion. This approach enables robust and efficient register verification for complex subsystems and saves significant time compared with the UVM register model.
To address this, a protocol-to-protocol AMBA bridge is developed. The bridge converts write commands from the verification intellectual property (VIP) into writes for the device under test (DUT) and reads data from the DUT, returning it to the corresponding VIP address. Because the DUT does not return data at the same address, address conversion logic with several finite state machines (FSMs) is implemented. This approach allows the VIP to perform checks as expected, despite the indirect read mechanism.
Counter value abstraction is used to manage delays and simplify verification, ensuring efficient completion. This approach enables robust and efficient register verification for complex subsystems and saves significant time compared with the UVM register model.
Event Type
Engineering Poster
TimeTuesday, July 285:00pm - 6:00pm PDT
LocationDAC Pavilion, Exhibit Floor