SynPSL: Behavioral Synthesis of PSL Assertions

The effort of verifying state-of-the-art hardware designs undeviatingly increases with the complexity of those designs. The design's state space, directly related to its complexity, grows exponentially, while the computational performance for verifying the design grows only linearly. This so-called verification gap can, for example, be met by using methods such as assertion-based verification (ABV), which can be used for both specifying the system's properties as well as verifying the relating implementation during simulation phase. In this paper, we present an open-source tool which generates synthesizable HDL code from assertions specified in the Property Specification Language (PSL). This is done by first reducing the PSL formulas into base cases, called PSLmin, and then generating automata which can be transformed to synthesizable HDL code and therefore into hardware.