PSL (język opisu właściwości)

Z Wikipedii

PSL (ang. Property Specification Language) jest językiem opisu właściwości układów i systemów elektronicznych, kontrolowanym przez standard IEEE Std. 1850.

[edytuj] Historia

Język zaczął powstawać w roku 1994 w izraelskim oddziale firmy IBM (IBM Haifa Research Laboratory) pod nazwą Sugar. Początkowo stanowił składniowe uproszczenie logiki temporalnej CTL używanej w wewnętrznych projektach firmy. Z biegem czasu język został wzbogacony o nowe operatory i wyrażenia regularne. W marcu 2001 Sugar 1.0 został przekazany organizacji Accellera jako jeden z kandydatów na standardowy język opisu właściwości (ang. property language). Sugestie Accellery spowodowały dodanie elementów logiki temporalnej LTL do języka. W ten sposób ulepszony Sugar 2.0 został wybrany w kwietniu 2002 jako podstawa dla powstającego nowego standardu. W czerwcu 2004 Accellera zaaprobowała nowy standard, nazwany PSL 1.1, i przekazała go do IEEE w celu dalszej standardyzacji. Prace nad językiem pod auspicjami IEEE postępowały szybko i pierwsza wersja standardu 1850 została zaaprobowana we wrześniu 2005.

[edytuj] Opis

PSL pozwala opisywać właściwości układów na wielu poziomach:

• poziom logiki boolowskiej z typowymi funkcjami AND, OR, NOT i.t.p.
• poziom logiki temporalnej, wprowadzający pojęcie czasu i sekwencji zdarzeń
• poziom weryfikacji, pozwalający na kontrolowanie wymuszeń podczas symulacji (dyrektywa assume), sygnalizację błędów (dyrektywa assert) i testowanie pokrycia (dyrektywa cover)
• poziom modelowania, umożliwiający opis zachowania wejść, sygnałów i zmiennych (głównie na potrzeby narzędzi weryfikacji formalnej)

W celu ułatwienia współpracy z symulatorami i narzędziami używającymi innych języków, PSL występuje w różnych wariantach (ang. flavors) zbliżonych składniowo do VHDLa, Veriloga, SystemVeriloga czy też SystemC. Na przykład w wariancie VHDLowym jest możliwe używanie operatora logicznego 'and', a w wariancie Verilogowym - operatora '&&'.

Proste wyrażenia logiczne w PSLu (podobnie jak i w innych językach) pozwalają opisać stan ustalony układu. Sekwencje opisują zmiany zachodzące w układzie (n.p. przejście automatu ze stanu A do stanu B), więc mogą być w uproszczeniu traktowane jako wyrażenia logiczne z dodanym wymiarem czasu. Kombinacje wyrażeń logicznych i sekwencji tworzone przy użyciu operatorów temporalnych są nazywane właściwościami (ang. properties). Zarówno sekwencje, jak i właściwości mogą być w PSLu zdefiniowane jako samodzielne obiekty z unikalną nazwą i zestawem parametrów.

Dyrektywy języka PSL używają właściwości zdefiniowane dla danego układu w procesie jego weryfikacji. Właściwości, które powinny być zawsze prawdziwe (asercje), są weryfikowane przy użyciu dyrektywy assert produkującej komunikaty błędu w przypadku nie spełnienia właściwości. Właściwości opisujące pożądane wymuszenia dla danego układu są weryfikowane przy użyciu dyrektywy assume (ta dyrektywa jest dostępna podczas weryfikacji formalnej). W celu sprawdzenia czy dana właściwość była kiedykolwiek sprawdzana przez narzędzie weryfikacji można użyć dyrektywy cover; w tym przypadku brak jakichkolwiek komunikatów oznacza negatywny wynik testu pokrycia i sugeruje zmiany w procesie weryfikacji.

Jednym z charakterystycznych elementów PSL są SERE (ang. Sequential Extended Regular Expressions = rozszerzone sekwencyjne wyrażenia regularne), obejmujące proste wyrażenia logiczne, sekwencje, i ich kombinacje z użyciem operatorów logicznych i temporalnych. SERE w PSLu są zapisywane w nawiasach klamrowych. Przykładem SERE może być {A;B[*3];C}, które oznacza w języku potocznym: sygnał A jest aktywny przez jeden cykl, następnie sygnał B jest aktywny przez 3 cykle, po czym sygnał C jest aktywny przez jeden cykl.

SERE często wymagają zdefiniowania sygnału taktującego (zegara), którego aktywne zbocze określa moment pobrania wartości sygnałów występujących w SERE. Zegar może być zdefiniowany jako sygnał globalny, domyślny dla wszystkich wyrażeń, albo oddzielnie dla każdego wyrażenia. Przykładowe SERE użyte w poprzednim paragrafie można rozbudować do {A;B[*3];C}@rose(CLK), gdzie rose(CLK) oznacza że wyrażenie jest taktowane rosnącym zboczem sygnału CLK.