Property Specification Language
From Wikipedia, the free encyclopedia
Cet article est une ébauche concernant l’informatique.
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.
Les assertions peuvent ensuite être interprétées par un moteur de simulation (vérification dynamique) ou un outil de vérification formelle (vérification statique) qui supporte le langage. Le PSL permet également de relever le nombre de mise à l'épreuve d'une propriété lors d'une simulation ou d'une analyse. Cela permet, en fin de phase de vérification, de justifier du taux de couverture réalisé.
