Addressing Ordering Woes of PCIe with Formal Verification
TimeTuesday, July 12th6pm - 7pm PDT
LocationLevel 2 Lobby
Event Type
Networking Reception
Work-in-Progress Poster
DescriptionThe potential of formal verification is harnessed the best when it is applied on blocks and functionalities which are best suited for the formal technology. Transaction ordering, data integrity and deadlock detection are such features which are critical to PCIe based design IPs that facilitates high-bandwidth data transportation in complex SOCs. On one side when violation of ordering can cause data corruption; on the other, the same ordering rules may block transactions unrelated to any Producer/Consumer transaction
sequence. Transaction ID based relaxed ordering is a significant optimization to save the day. Relaxed ordering gives switches and the root complex permission to move certain transaction ahead of others; an action which is normally prohibited. Such optimization adds to the complexity of maintaining overall rules of transaction ordering. Formal verification is well-suited for exploring numerous scenarios of transaction ordering in such data transportation blocks. In this paper, the primary aim is to explain a methodology to verify ordering requirements between the Producer/Consumer transaction sequence especially considering the case of relax ordering if allowed. Furthermore, we will also touch upon on performance validation using safety properties and usage of formal scoreboard for verifying transaction ordering.