Egenskapsspecifikationsspråk

Property Specification Language ( PSL ) är en temporal logik som utökar linjär temporal logik med en rad operatorer för både enkel uttryck och förbättring av uttryckskraft. PSL använder sig i stor utsträckning av reguljära uttryck och syntaktisk sugaring. Det används ofta inom hårdvarudesign- och verifieringsindustrin, där formella verifieringsverktyg (som modellkontroll ) och/eller logiska simuleringsverktyg används för att bevisa eller motbevisa att en given PSL-formel håller för en given design.

PSL utvecklades ursprungligen av Accellera för att specificera egenskaper eller påståenden om hårdvarudesigner. Sedan september 2004 standardiseringen av språket gjorts i IEEE 1850-arbetsgruppen. I september 2005 tillkännagavs IEEE 1850 Standard for Property Specification Language (PSL).

Syntax och semantik

PSL kan uttrycka att om något scenario inträffar nu, så bör ett annat scenario inträffa en tid senare. Till exempel kan egenskapen "en begäran ska alltid så småningom beviljas " uttryckas med PSL-formeln:

alltid (begäran -> så småningom! bevilja)

Egenskapen "varje begäran som omedelbart följs av en ack -signal, bör följas av en fullständig dataöverföring , där en fullständig dataöverföring är en sekvens som börjar med signalstart , slutar med signalslut där upptaget håller på under tiden" uttryckt med PSL-formeln:

(true[*]; req; ack) |=> (start; upptagen[*]; slut)

Ett spår som uppfyller denna formel ges i figuren till höger.

ett enkelt spår tillfredsställande

(true[*]; req; ack) |=> (start; upptagen[*]; slut)

PSL:s temporala operatörer kan grovt klassificeras i operatörer av LTL-stil och operatörer av vanligt uttryck . Många PSL-operatörer finns i två versioner, en stark version, indikerad med ett utropsteckens suffix ( ! ), och en svag version. Den starka versionen ställer eventualitetskrav (dvs kräver att något kommer att hålla i framtiden), medan den svaga versionen inte gör det. Ett understreckssuffix ( _ ) används för att skilja inkluderande och icke-inkluderande krav. Suffixen _a och _e används för att beteckna universella (alla) kontra existentiella (finns) krav. Exakta tidsfönster betecknas med [n] och flexibla med [m..n] .

Operatörer i SERE-stil

Den vanligaste PSL-operatören är operatorn "suffix-implication" (även känd som "triggers"-operatorn), som betecknas med | => . Dess vänstra operand är ett reguljärt PSL-uttryck och dess högra operand är vilken PSL-formel som helst (vare sig det är i LTL-stil eller reguljärt uttryck). Semantiken för r |=> p är att vid varje tidpunkt i så att sekvensen av tidpunkter fram till i utgör en matchning med det reguljära uttrycket r, bör vägen från i+1 uppfylla egenskapen p. Detta exemplifieras i figurerna till höger.

path satisfying r triggar p på två icke-överlappande sätt

path satisfying r triggar p på två överlappande sätt

path satisfying r triggar p på tre sätt

De reguljära uttrycken för PSL har de vanliga operatorerna för sammanlänkning ( ; ), Kleene-closure ( * ), och union ( | ), samt operator för fusion ( : ), intersection ( && ) och en svagare version ( & ), och många variationer för konsekutiv räkning [*n] och inkonsekutiv räkning t.ex. [=n] och [->n] .

Triggeroperatorn finns i flera varianter, som visas i tabellen nedan.

Här är s och t PSL-reguljära uttryck, och p är en PSL-formel.

s \|=> t!	om det finns en matchning av s, så finns det en matchning av t på suffixet av spåret, t startar cykeln efter s slut, matchen av t måste nå sitt slut
s \|-> t!	om det finns en matchning av s, så finns det en matchning av t på suffixet av spåret, t startar samma cykel som slutar, matchen av t måste nå sitt slut
s \|=> t	om det finns en matchning av s, så finns det en matchning av t på suffixet av spåret, t startar cykeln efter s slut, matchningen av t kan "fastna" i mitten
s \|-> t	om det finns en matchning av s, så finns det en matchning av t på suffixet av spåret, t startar samma cykel som slutar, matchningen av t kan "fastna" i mitten

Operatörer för sammanlänkning, sammansmältning, sammanfogning, korsning och deras variationer visas i tabellen nedan.

Här är s och t PSL reguljära uttryck.

`s ; t`	matchning av s följt av en matchning av t, t startar cykeln efter att s slutar
`s: t`	matchning av s följt av en matchning av t, t startar samma cykel som s slutar
`s \| t`	match av s eller match av t
`s && t`	matchning av s och matchning av t, varaktigheten av båda är av samma längd
`s & t`	matchning av s och matchning av t, varaktighet matcher kanske olika
`s inom t`	matchning av s inom en matchning av t, förkortning av ([]; s; []) && t

Operatörer för på varandra följande repetitioner visas i tabellen nedan.

Här är ett reguljärt PSL-uttryck.

`si]`	i på varandra följande upprepningar av s
`s[*i..j]`	mellan i till j på varandra följande upprepningar av s
`si..]`	åtminstone i till på varandra följande upprepningar av s
`s[*]`	noll eller fler på varandra följande upprepningar av s
`s[+]`	en eller flera på varandra följande upprepningar av s

Operatörer för icke-konsekutiva repetitioner visas i tabellen nedan.

Här är b vilket booleskt PSL-uttryck som helst.

`b[=i]`	i inte nödvändigtvis på varandra följande upprepningar av b, motsvarande (!b[];b)[i]; !b[*]
`b[=i..j]`	åtminstone i och inte mer än j inte nödvändigtvis på varandra följande upprepningar av b, motsvarande (!b[];b)[i..j]; !b[*]
`b[=i..]`	åtminstone i inte nödvändigtvis på varandra följande upprepningar av b, motsvarande (!b[];b)[i..]; !b[*]
`b[->m]`	m inte nödvändigtvis på varandra följande upprepningar av b som slutar med b, motsvarande (!b[];b)[m]
`b[->m:n]`	minst m och inte fler än n inte nödvändigtvis på varandra följande upprepningar av b som slutar med b, motsvarande (!b[];b)[m..n]
`b[->m..]`	åtminstone m inte nödvändigtvis på varandra följande upprepningar av b som slutar med b, motsvarande (!b[];b)[m..]; !b[*]
`b[->]`	genväg för b[->1], motsvarande (!b[*];b)

LTL-liknande operatörer

Nedan är ett exempel på några LTL-liknande operatörer av PSL.

Här är p och q alla PSL-formler.

`alltid sid`	egenskapen p gäller varje tidpunkt
`aldrig sid`	egenskapen p gäller inte någon tidpunkt
`så småningom! sid`	det finns en framtida tidpunkt där p gäller
`Nästa! sid`	det finns en nästa tidpunkt, och p håller på denna punkt
`nästa sid`	om det finns en nästa tidpunkt, så gäller p på denna punkt
`nästa![n] sid`	det finns en n:te tidpunkt, och p gäller på denna punkt
`nästa[n] sid`	om det finns en n:te tidpunkt, så gäller p på denna punkt
`nästa_e![m..n] sid`	det finns en tidpunkt, inom m-te till n-te från strömmen där p gäller.
`nästa_e[m..n] sid`	om det finns åtminstone n:te tidpunkter, så gäller p en av de m:te till n:te punkterna.
`nästa_a![m..n] sid`	det finns åtminstone n fler tidpunkter och p gäller alla tidpunkter mellan m:te och n:te, inklusive.
`nästa_a[m..n] sid`	p håller på alla nästa m-te till n-te tidpunkter, hur många som helst
`p tills! q`	det finns en tidpunkt där q håller, och p håller tills den tidpunkten
`p tills q`	p håller tills en tidpunkt där q håller, om en sådan finns
`p tills!_ q`	det finns en tidpunkt där q håller, och p håller tills den tidpunkten och i den tidpunkten
`p tills_ q`	p håller tills en tidpunkt där q gäller, och i den tidpunkten, om sådan finns
`p innan! q`	p gäller strikt före den tidpunkt där q gäller, och p slutligen gäller
`p före q`	p håller strikt före den tidpunkt där q gäller, om p aldrig håller, så gör inte q heller
`p före!_ q`	p håller före eller vid samma tidpunkt där q håller, och p till slut håller
`p före_ q`	p håller före eller vid samma tidpunkt där q håller, om p aldrig håller, så gör inte q heller

Provtagningsoperatör

Ibland är det önskvärt att ändra definitionen av nästa tidpunkt , till exempel i flerklockade mönster, eller när en högre abstraktionsnivå önskas. Samplingsoperatorn (även känd som klockoperatorn ), betecknad @ , används för detta ändamål. Formeln p @ c där p är en PSL-formel och c ett PSL booleska uttryck håller på en given väg om p på den vägen projiceras på de cykler i vilka c gäller, som exemplifieras i figurerna till höger.

sökväg och formel som visar behovet av en samplingsoperator

Den första egenskapen säger att "varje begäran som omedelbart följs av en ack -signal, bör följas av en fullständig dataöverföring , där en fullständig dataöverföring är en sekvens som börjar med signalstart , slutar med signalslut i vilken data ska innehålla minst 8 gånger:

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

Men ibland är det önskvärt att endast överväga de fall där ovanstående signaler uppstår på en cykel där clk är hög. Detta är avbildat i den andra figuren där även formeln

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

använder data[*3] och [*n] är konsekutiv upprepning, det matchande spåret har 3 icke-konsekutiva tidpunkter där data håller, men när man bara betraktar tidpunkterna där clk håller, blir tidpunkterna där data håller i följd.

sökväg och formel som visar effekten av samplingsoperatorn @

Semantiken för formler med kapslad @ är lite subtil. Den intresserade läsaren hänvisas till [2].

Avbryt operatörer

PSL har flera operatörer för att hantera trunkerade vägar (ändliga vägar som kan motsvara ett prefix i beräkningen). Trunkerade vägar förekommer vid kontroll av gränsad modell, på grund av återställningar och i många andra scenarier. Avbrytoperatorerna anger hur eventualiteter ska hanteras när en sökväg har trunkerats. De förlitar sig på den trunkerade semantiken som föreslås i [1].

Här är p valfri PSL-formel och b är valfritt PSL booleskt uttryck.

`p async_abort b`	antingen p håller eller p misslyckas inte förrän b håller; b känns igen asynkront
`p sync_abort b`	antingen p håller eller p misslyckas inte förrän b håller; b känns igen synkront
`p avbryt b`	motsvarande p async_abort b

Uttryckskraft

PSL subsumerar den tidsmässiga logiken LTL och utökar dess uttryckskraft till de omega-reguljära språken . Förstärkningen i uttryckskraft, jämfört med den för LTL, som har den uttryckskraft som de stjärnfria ω-reguljära uttrycken har, kan tillskrivas suffixets implikation , även känd som triggeroperatorn , betecknad "|->". Formeln r |-> f där r är ett reguljärt uttryck och f är en temporal logisk formel gäller för en beräkning w om något prefix av w som matchar r har en fortsättning som uppfyller f . Andra icke-LTL-operatörer för PSL är @ -operatören, för att specificera flerklockade konstruktioner, abort -operatorerna, för att hantera hårdvaruåterställningar och lokala variabler för korthet.

Skikten

PSL definieras i fyra lager: det booleska lagret , det temporala lagret , modelleringsskiktet och verifieringsskiktet .

Det booleska lagret används för att beskriva ett aktuellt tillstånd för designen och formuleras med hjälp av en av de ovan nämnda HDL:erna.
Det temporala lagret består av de temporala operatorerna som används för att beskriva scenarier som sträcker sig över tid (möjligen över ett obegränsat antal tidsenheter).
Modelleringsskiktet kan användas för att beskriva hjälptillståndsmaskiner på ett procedurmässigt sätt .
Verifieringsskiktet består av direktiv till ett verifieringsverktyg (till exempel för att hävda att en given egenskap är korrekt eller att anta att en viss uppsättning egenskaper är korrekt vid verifiering av en annan uppsättning egenskaper) .

Språkkompatibilitet

Egenskapsspecifikationsspråk kan användas med flera elektroniska systemdesignspråk (HDL) som:

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

När PSL används tillsammans med en av ovanstående HDL, använder dess booleska lager operatorerna för respektive HDL.

1850-2005 – IEEE Standard for Property Specification Language (PSL) . 2005. doi : 10.1109/IEEESTD.2005.97780 . ISBN 0-7381-4780-X .
- IEC 62531:2007 62531-2007 – IEC 62531 Ed. 1 (2007-11) (IEEE Std 1850-2005): Standard for Property Specification Language (PSL) . 2007. doi : 10.1109/IEEESTD.2007.4408637 . ISBN 978-0-7381-5727-6 .
1850-2010 – IEEE Standard for Property Specification Language (PSL) . 2010. doi : 10.1109/IEEESTD.2010.5446004 . ISBN 978-0-7381-6255-3 .
- IEC 62531:2012 62531-2012 – IEC 62531:2012(E) (IEEE Std 1850-2010): Standard for Property Specification Language (PSL) . 2012. doi : 10.1109/IEEESTD.2012.6228486 . ISBN 978-0-7381-7299-6 .
Eisner, Cindy; Fisman, Dana; Havlicek, John; Lustig, Yoad; McIsaac, Anthony; Van Campenhout, David (2003). "Resonera med temporär logik på trunkerade vägar" (PDF) . Datorstödd verifiering . Föreläsningsanteckningar i datavetenskap. Vol. 2725. sid. 27. doi : 10.1007/978-3-540-45069-6_3 . ISBN 978-3-540-40524-5 .
Eisner, Cindy; Fisman, Dana; Havlicek, John; McIsaac, Anthony; Van Campenhout, David (2003). "Definitionen av en temporär klockoperatör" (PDF) . Automater, språk och programmering . Föreläsningsanteckningar i datavetenskap. Vol. 2719. sid. 857. doi : 10.1007/3-540-45061-0_67 . ISBN 978-3-540-40493-4 .

externa länkar

Böcker på PSL