Property Specification Language
- Property Specification Language
-
Pour les articles homonymes,
voir PSL.
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 mai 2003, et par l’IEEE en septembre 2004.
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.
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 é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é.
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) permet de vérifier sur front montant de CLK qu'on n'a jamais SCLK=0 quand 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) permet de 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;
Notes et références
Wikimedia Foundation.
2010.
Contenu soumis à la licence CC-BY-SA. Source : Article Property Specification Language de Wikipédia en français (auteurs)
Regardez d'autres dictionnaires:
Property Specification Language — (PSL) is a language developed by Accellera for specifying properties or assertions about hardware designs. The properties can then be simulated or formally verified. Since September 2004 the standardization on the language has been done in IEEE… … Wikipedia
Property Specification Language — Die Property Specification Language (PSL), auf Deutsch etwa Beschreibungssprache für Eigenschaften , wurde von Accellera entwickelt, um Eigenschaften oder Assertions beim Entwurf von Hardware Designs zu spezifizieren. Diese Eigenschaften können… … Deutsch Wikipedia
Specification language — A specification language is a formal language used in computer science.Unlike most programming languages, which are directly executable formal languages used to implement a system, specification languages are used during systems analysis,… … Wikipedia
Hardware description language — In electronics, a hardware description language or HDL is any language from a class of computer languages and/or programming languages for formal description of electronic circuits. It can describe the circuit s operation, its design and… … Wikipedia
Object Constraint Language — The Object Constraint Language (OCL) is a declarative language for describing rules that apply to Unified Modeling Language (UML) models developed at IBM and now part of the UML standard. Initially, OCL was only a formal specification language… … Wikipedia
Java Modeling Language — The Java Modeling Language (JML) follows the design by contract paradigm. It is a specification language for Java programs, using . There are various verification tools for JML, such as a runtime assertion checker and the Extended Static Checker… … Wikipedia
Geography Markup Language — A vector map, with points, polylines and polygons. Filename extension .gml or .xml Internet media type application/gml+xml[1 … Wikipedia
Web Ontology Language — OWL Web Ontology Language Current Status Published Year Started 2002 Editors Mike Dean, Guus Schreiber Base Standards Resource Description Framework, RDFS Domain Semantic Web A … Wikipedia
Oxygene (programming language) — Oxygene Developer RemObjects Software Stable release 3.0.21 (August 29, 2009; 2 years ago (2009 08 29)) Influenced by Object Pas … Wikipedia
Glossary of Unified Modeling Language terms — This glossary of Unified Modeling Language terms covers all versions of UML. Individual entries will point out any distinctions that exist between versions.A* Abstract An indicator applied to a classifier (e.g., actor, class, use case) or to some … Wikipedia
