SynPSL: Behavioral Synthesis of PSL Assertions

摘要

The effort of verifying state-of-the-art hardware designs un-deviatingly 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.rnIn this paper, we present an open-source tool which generates synthe-sizable HDL code from assertions specified in the Property Specification Language (PSL). This is done by first reducing the PSL formulas into base cases, called PSL_(min), and then generating automata which can be transformed to synthesizable HDL code and therefore into hardware.