Property Specification Language

El llenguatge d'especificació de propietats (PSL) és una lògica temporal que amplia la lògica temporal lineal amb un ventall d'operadors tant per facilitar l'expressió com per millorar el poder expressiu. PSL fa un ús extensiu d'expressions regulars i de sucre sintàctic. S'utilitza àmpliament a la indústria del disseny i verificació de maquinari, on s'utilitzen eines de verificació formal (com ara la verificació de models) i/o eines de simulació lògica per demostrar o refutar que una fórmula PSL determinada s'aplica a un disseny determinat.

PSL va ser desenvolupat inicialment per Accellera per especificar propietats o afirmacions sobre dissenys de maquinari. Des de setembre de 2004 l' estandardització de l'idioma es fa en el grup de treball IEEE 1850. El setembre de 2005, es va anunciar l'estàndard IEEE 1850 per al llenguatge d'especificació de propietats (PSL).

Sintaxi i semàntica

PSL pot expressar que si un escenari passa ara, un altre escenari hauria de passar un temps després. Per exemple, la propietat "arequest sempre hauria de ser-hogrant ed" es pot expressar mitjançant la fórmula PSL:

 always (request -> eventually! grant)

La propietat "totsrequest que va seguida immediatament d'unacksenyal , ha d'anar seguit d'un completdata transfer, on una transferència de dades completa és una seqüència que comença amb senyal start, acaba amb senyalend en què busy mentre tant " es pot expressar amb la fórmula PSL:

 (true[*]; req; ack) |=> (start; busy[*]; end)

A la figura de la dreta es dóna un rastre que satisfà aquesta fórmula.

una simple traça satisfactòria

(true[*]; req; ack) |=> (start; busy[*]; end)

(true[*]; req; ack) |=> (start; busy[*]; end)

Els operadors temporals de PSL es poden classificar aproximadament en operadors d'estil LTL i operadors d'estil d'expressió regular. Molts operadors de PSL vénen en dues versions, una versió forta, indicada amb un sufix de signe d'exclamació (!), i una versió feble. La versió forta fa requisits d'eventualitat (és a dir, requereix que alguna cosa es mantingui en el futur), mentre que la versió feble no. Un sufix de subratllat (_) s'utilitza per diferenciar requisits inclusius i no inclusius. Els sufixos _a i _e s'utilitzen per denotar requisits universals (tots) versus requisits existencials (existents). Les finestres de temps exactes es denoten per[n] i flexible per[m..n].

Operadors d'estil SERE

El camí que satisfà r activa p de dues maneres no solapades

L'operador PSL més utilitzat és l'operador "implicació de sufix" (també conegut com a operador "disparadors"), que es denota per|=>. El seu operand esquerre és una expressió regular PSL i el seu operand dret és qualsevol fórmula PSL (ja sigui en estil LTL o estil d'expressió regular). La semàntica der |=> p és que en cada punt de temps i tal que la seqüència de punts de temps fins a i constitueix una coincidència amb l'expressió regular r, el camí des de i+1 hauria de satisfer la propietat p. Això s'exemplifica a les figures de la dreta.

El camí que satisfà r activa p de dues maneres superposades

Les expressions regulars de PSL tenen els operadors comuns per a la concatenació (;), tancament Kleene (*), i unió (|), així com l'operador de fusió (:), intersecció (&& ) i una versió més feble (& ), i moltes variacions per al recompte consecutiu[*n] i recompte consecutiu p.ex: [=n] i[->n].

El camí que satisfà r activa p de tres maneres

Operador de mostreig

De vegades és desitjable canviar la definició del següent punt de temps, per exemple, en dissenys de cronometratge múltiple, o quan es desitja un nivell d'abstracció més alt. L' operador de mostreig (també conegut com a operador de rellotge), indicat @, s'utilitza amb aquesta finalitat. La fórmula p @ c on p és una fórmula PSL i c expressions booleanes PSL es mantenen en un camí donat sip en aquell camí projectat sobre els cicles en quèc sosté, com s'exemplifica a les figures de la dreta.

Camí i fórmula que mostren la necessitat d'un operador de mostreig

La primera propietat estableix que "totsrequest que va seguida immediatament d'un senyal ack, ha d'anar seguit d'un complet data transfer, on una transferència de dades completa és una seqüència que comença amb senyal start, acaba amb senyal end en què data han de contenir almenys 8 vegades:

 (true[*]; req; ack) |=> (start; data[=8]; end)

Però de vegades es vol considerar només els casos en què els senyals anteriors es produeixen en un cicle onclk és alt. Això es mostra a la segona figura en què encara que la fórmula

 ((true[*]; req; ack) |=> (start; data[*3]; end)) @ clk

usa data[*3] i [*n] és repetició consecutiva, la traça coincident té 3 punts de temps no consecutius on data es mantenen, però si es consideren només els punts de temps on clk es manté, els punts de temps on data la retenció esdevé consecutiva.

Camí i fórmula que mostren l'efecte de l'operador de mostreig @

Capes

PSL es defineix en 4 capes: la capa booleana, la capa temporal, la capa de modelatge i la capa de verificació.

• La capa booleana s'utilitza per descriure l'estat actual del disseny i es formula amb un dels HDL esmentats anteriorment.
• La capa temporal consisteix en els operadors temporals utilitzats per descriure escenaris que s'estenen al llarg del temps (possiblement en un nombre il·limitat d'unitats de temps).
• La capa de modelatge es pot utilitzar per descriure màquines d'estat auxiliars d'una manera procedimental.
• La capa de verificació consta de directives a una eina de verificació (per exemple, per afirmar que una propietat determinada és correcta o per suposar que un determinat conjunt de propietats és correcte quan es verifica un altre conjunt de propietats).

Compatibilitat de llenguatges

El llenguatge d'especificació de propietats es pot utilitzar amb diversos llenguatges de disseny de sistemes electrònics (HDL), com ara:

• VHDL (IEEE 1076)
• Verilog (IEEE 1364)
• SystemVerilog (IEEE 1800)
• SystemC (IEEE 1666) per Open SystemC Initiative (OSCI).

Quan s'utilitza PSL juntament amb un dels HDL anteriors, la seva capa booleana utilitza els operadors del HDL respectiu.