Le Property Specification Language (PSL) (en français : Langage de spécification par propriétés) est basé sur le langage Sugar d’IBM. Il a été approuvé par l’organisme Accellera en , et par l’IEEE[1] en .
C'est un langage formel qui permet de réaliser une spécification matérielle à l'aide de propriétés et d'assertions. Du fait de la haute précision mathématique du langage, l'opération de description retire toute ambiguïté à la spécification résultante. C'est un langage rapide à assimiler, basé sur une syntaxe relativement simple.