Assertion based verification using PSL-like properties in Haskell

With the increasing complexity of designs, the verification costs grow considerably. Using Assertion Based Verification with assertions implemented on real hardware, can speed up the verification process. Property Specification Language is one of the common standards for describing formal properties and specifications of a design. We implemented a subset of PSL operations in Haskell in this work. A functional programming language like Haskell can appear as an advantageous choice for formal verification and high-level descriptions. We use the implemented PSL operators to set up different synthesizable PSL properties. The implemented PSL operators are tested on an FPGA for an AMBA AHB-based system which is also implemented in Haskell.