El lenguaje de especificación de propiedades ( PSL ) es una lógica temporal que extiende la lógica temporal lineal con una variedad de operadores para facilitar la expresión y mejorar el poder expresivo. El PSL hace un uso extensivo de expresiones regulares y de sintaxis. Se utiliza ampliamente en la industria de diseño y verificación de hardware, donde se utilizan herramientas de verificación formal (como la verificación de modelos ) y/o herramientas de simulación lógica para probar o refutar que una fórmula PSL dada se cumple en un diseño determinado.
El lenguaje PSL fue desarrollado inicialmente por Accellera para especificar propiedades o afirmaciones sobre diseños de hardware. Desde septiembre de 2004, la estandarización del lenguaje se ha llevado a cabo en el grupo de trabajo IEEE 1850. En septiembre de 2005, se anunció el estándar IEEE 1850 para lenguaje de especificación de propiedades (PSL).
La PSL puede expresar que si ocurre un escenario ahora, entonces otro escenario debería ocurrir algún tiempo después. Por ejemplo, la propiedad "una solicitud siempre debería ser eventualmente concedida " puede expresarse mediante la fórmula de la PSL:
siempre (solicitud -> eventualmente! concesión)La propiedad "cada solicitud que es seguida inmediatamente por una señal de reconocimiento , debe ser seguida por una transferencia de datos completa , donde una transferencia de datos completa es una secuencia que comienza con la señal start y termina con la señal end en la que la señal busy se mantiene mientras tanto" se puede expresar mediante la fórmula PSL:
(verdadero[*]; solicitud; confirmación) |=> (inicio; ocupado[*]; fin)En la figura de la derecha se da una traza que satisface esta fórmula.
(verdadero[*]; solicitud; confirmación) |=> (inicio; ocupado[*]; fin)Los operadores temporales de PSL se pueden clasificar a grandes rasgos en operadores de estilo LTL y operadores de estilo de expresión regular . Muchos operadores de PSL vienen en dos versiones, una versión fuerte, indicada por un sufijo de signo de exclamación ( ! ), y una versión débil. La versión fuerte hace requisitos de eventualidad (es decir, requiere que algo se mantenga en el futuro), mientras que la versión débil no lo hace. Un sufijo de guión bajo ( _ ) se utiliza para diferenciar los requisitos inclusivos de los no inclusivos . Los sufijos _a y _e se utilizan para denotar requisitos universales (todos) frente a requisitos existenciales (existen). Las ventanas de tiempo exactas se denotan por [n] y las flexibles por [m..n] .
El operador PSL más comúnmente utilizado es el operador de "implicación de sufijo" (también conocido como el operador de "activadores"), que se denota por |=> . Su operando izquierdo es una expresión regular PSL y su operando derecho es cualquier fórmula PSL (ya sea en estilo LTL o en estilo de expresión regular). La semántica de r |=> p es que en cada punto de tiempo i tal que la secuencia de puntos de tiempo hasta i constituya una coincidencia con la expresión regular r, la ruta desde i+1 debe satisfacer la propiedad p. Esto se ejemplifica en las figuras de la derecha.
Las expresiones regulares de PSL tienen operadores comunes para concatenación ( ; ), cierre de Kleene ( * ) y unión ( | ), así como operadores para fusión ( : ), intersección ( && ) y una versión más débil ( & ), y muchas variaciones para conteo consecutivo [*n] y conteo no consecutivo, por ejemplo [=n] y [->n] .
El operador de activación viene en varias variaciones, que se muestran en la siguiente tabla.
Aquí s y t son expresiones regulares de PSL, y p es una fórmula de PSL.
Los operadores de concatenación, fusión, unión, intersección y sus variaciones se muestran en la siguiente tabla.
Aquí s y t son expresiones regulares de PSL.
Los operadores para repeticiones consecutivas se muestran en la siguiente tabla.
Aquí hay una expresión regular de PSL.
Los operadores para repeticiones no consecutivas se muestran en la siguiente tabla.
Aquí b es cualquier expresión booleana PSL.
A continuación se muestra una muestra de algunos operadores de estilo LTL de PSL.
Aquí p y q son fórmulas PSL.
A veces es conveniente cambiar la definición del siguiente punto temporal , por ejemplo, en diseños con múltiples relojes, o cuando se desea un nivel de abstracción más alto. El operador de muestreo (también conocido como operador de reloj ), denotado @ , se utiliza para este propósito. La fórmula p @ c donde p es una fórmula PSL y c una expresión booleana PSL se cumple en una ruta dada si p en esa ruta proyectada sobre los ciclos en los que c se cumple, como se ejemplifica en las figuras a la derecha.
La primera propiedad establece que "cada solicitud que es seguida inmediatamente por una señal ack , debe ser seguida por una transferencia de datos completa , donde una transferencia de datos completa es una secuencia que comienza con la señal start y termina con la señal end en la que los datos deben contener al menos 8 veces:
(verdadero[*]; req; ack) |=> (inicio; datos[=8]; fin)Pero a veces es conveniente considerar solo los casos en los que las señales anteriores se producen en un ciclo en el que el clk es alto. Esto se representa en la segunda figura en la que, aunque la fórmula
((verdadero[*]; req; ack) |=> (inicio; datos[*3]; fin)) @ clkusa datos[*3] y [*n] es repetición consecutiva, el rastro coincidente tiene 3 puntos de tiempo no consecutivos donde se mantienen los datos , pero al considerar solo los puntos de tiempo donde se mantienen los datos , los puntos de tiempo donde se mantienen los datos se vuelven consecutivos.
La semántica de las fórmulas con @ anidadas es un poco sutil. El lector interesado puede consultar [2].
PSL tiene varios operadores para tratar con rutas truncadas (rutas finitas que pueden corresponder a un prefijo del cálculo). Las rutas truncadas ocurren en la verificación de modelos acotados, debido a reinicios y en muchos otros escenarios. Los operadores de aborto especifican cómo se deben tratar las eventualidades cuando se trunca una ruta. Se basan en la semántica de truncamiento propuesta en [1].
Aquí p es cualquier fórmula de PSL y b es cualquier expresión booleana de PSL.
El PSL subsume la lógica temporal LTL y extiende su poder expresivo al de los lenguajes omega-regulares . El aumento en el poder expresivo, comparado con el de LTL, que tiene el poder expresivo de las expresiones ω-regulares sin asterisco, puede atribuirse a la implicación de sufijo , también conocida como el operador de disparadores , denotado "|->". La fórmula r |-> f donde r es una expresión regular y f es una fórmula de lógica temporal se cumple en un cálculo w si cualquier prefijo de w que coincida con r tiene una continuación que satisface f . Otros operadores no LTL de PSL son el operador @ , para especificar diseños con múltiples relojes, los operadores de aborto , para tratar con reinicios de hardware, y las variables locales para mayor concisión.
PSL se define en 4 capas: la capa booleana , la capa temporal , la capa de modelado y la capa de verificación .
El lenguaje de especificación de propiedades se puede utilizar con múltiples lenguajes de diseño de sistemas electrónicos (HDL) como:
Cuando PSL se utiliza junto con uno de los HDL anteriores, su capa booleana utiliza los operadores del HDL respectivo.