Structured Approach to Property Specification and Verification of HW IP

Formal property specification and model checking are increasingly deployed in the HW design industry, thanks to the emergence of standard property specification languages and major advances in the maturity of model checking tools. Moderately sized HW IP is now within the capacity of such tools. Complete formal verification of such IP requires not only efficient algorithms, but also a systematic approach to specifying the properties of common classes of designs. This paper addresses the methodological aspects of such an approach in an industrial setting, the Random Number Generator IP. The PSL implementation and checking considerations are dealt with including the randomness preservation property which can not be tackled by the usual specification and verification methods.