Property Specification Language

Le Property Specification Language est basé sur le langage Sugar d'IBM. Il a été accepté par l'organisme Accellera en mai 2003, et par l'IEEE en septembre 2004.



Catégories :

Génie logiciel - Format de données numériques - Conception électronique - Électronique - Langage informatique

Page(s) en rapport avec ce sujet :

  • PSL Property Specification Language Reference Manual.... Untitled - A Formal Framework for Modular Composition, and Verification and Validation of.... matériels Motivation - Depuis 2000 : développement du langage de propriétés PSL, .... (source : fichier-pdf)
  • ... PSL : (Property Specification Language) est basé sur le langage Sugar... du projet AFCIM qui permet la vérification de propriétés LTL dans ... (source : )
  • PSL, pour Property specification language, est un langage d'assertions ou de ... issu du langage Sugar d'IBM, utilisé dans le cadre de la vérification de ... (source : electronique)

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é accepté par l'organisme Accellera en mai 2003, et par l'IEEE en septembre 2004.

C'est un langage formel qui sert à réaliser une spécification matérielle avec 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 assez simple.

Son utilisation

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 aussi 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é.

Inclus dans le code VHDL

library ieee;
use ieee.std_logic_1164.all;
entity receiver is
 port (clk       : in  std_logic; 
          ()
          B       : in std_logic;
          C       : in std_logic);
end reciver;
architecture archi of reciver is
Begin
-- Commentaires VHDL
-- psl default clock is rose(clk);
-- psl assert always (A->next(B));
-- psl assert always A->E before B;
-- psl C_then_FC: assert always C|=>{F[->2];C}; 
    (VHDL)
end archi;

Exemple en PSL

Cette unité de verification (vunit) sert à vérifier sur front montant de CLK qu'on n'a jamais SCLK=0 lorsque CS_N=1 :

vunit checker_spi(top)
  default clock : posedge(CLK);
  property p0 : never(!SCLK && CS_N);
  d0 : assert p0;


Cette unité de verification (vunit) sert à vérifier sur front montant de CLK qu'on a 8 coup d'horloge SCLK après le pasage à 0 de CS_N :

vunit checker_spi(top)
  default clock : posedge(CLK);
  sequence fe_CS_N : {CS_N;!CS_N};
  property p0 : always({fe_CS_N} |-> {SCLK;{!SCLK;SCLK}[*8]});
  d0 : assert p0;


Environnement de développement

Quelques fabricants proposent une version gratuite mais limitée de leurs outils.

Éditeur Produit Licence Synthétiseur Simulateur Remarques
Dolphin Integration SMASH[1] Propriétaire, gratuite Non Oui Simulateur SMASH Discovery gratuit

Notes et références

Recherche sur Amazon (livres) :



Ce texte est issu de l'encyclopédie Wikipedia. Vous pouvez consulter sa version originale dans cette encyclopédie à l'adresse http://fr.wikipedia.org/wiki/Property_Specification_Language.
Voir la liste des contributeurs.
La version présentée ici à été extraite depuis cette source le 07/04/2010.
Ce texte est disponible sous les termes de la licence de documentation libre GNU (GFDL).
La liste des définitions proposées en tête de page est une sélection parmi les résultats obtenus à l'aide de la commande "define:" de Google.
Cette page fait partie du projet Wikibis.
Accueil Recherche Aller au contenuDébut page
ContactContact ImprimerImprimer liens d'évitement et raccourcis clavierAccessibilité
Aller au menu