SVA PAPER: DYNAMIC DATA STRUCTURES IN ASSERTIONS
The integration of dynamic data structures, such as queues and associative arrays, into SystemVerilog assertions has sparked ongoing discussion in the hardware verification community. While these constructs enhance assertion capabilities, their support across EDA tools is inconsistent.
This paper addresses the challenges posed by the lack of uniform support for dynamic structures in SVA among tool vendors. It examines the current state of assertion support in major EDA tools, revealing disparities in handling queues and associative arrays. This inconsistency raises questions about the necessity and practicality of these complex structures in assertions.
Despite concerns, the benefits of using queues and associative arrays in specific verification scenarios are significant. The paper explores methods to implement these data structures in assertions, even without direct tool support. It presents techniques for efficient support logic, enabling verification engineers to utilize these structures while maintaining portability and performance.
Additionally, the paper demonstrates these techniques with a simulateable example and explores synthesizable logic as an alternative approach for formal verification environments. This solution aims to bridge the gap between simulation-based and formal verification methodologies.