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. PSL hace un uso extensivo de expresiones regulares y azúcar sintáctico. Se usa ampliamente en la industria de verificación y diseño de hardware, donde se utilizan herramientas de verificación formales (como la verificación de modelos ) y / o herramientas de simulación lógica para probar o refutar que una fórmula de PSL determinada se aplica a un diseño determinado.
PSL fue desarrollado inicialmente por Accellera para especificar propiedades o afirmaciones sobre diseños de hardware. Desde septiembre de 2004, la estandarización del idioma se ha realizado 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).
Sintaxis y semántica
PSL puede expresar que si algún escenario ocurre ahora, otro escenario debería ocurrir algún tiempo después. Por ejemplo, la propiedad "una solicitud siempre debería eventualmente ser concedido "puede expresarse mediante la fórmula PSL:
siempre (solicitud -> eventualmente! concesión)
La propiedad "cada solicitud que es seguida inmediatamente por una señal de confirmación , debe ir seguida de una transferencia de datos , donde una transferencia de datos completa es una secuencia que comienza con la señal comenzar , terminar con señal final en el cual ocupados, mientras tanto, "se puede expresar mediante la fórmula PSL:
(verdadero [*]; req; ack) | => (inicio; ocupado [*]; final)
En la figura de la derecha se muestra una traza que satisface esta fórmula.
Los operadores temporales de PSL se pueden clasificar aproximadamente 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. Un sufijo de subrayado ( _ ) Se utiliza para diferenciar incluido vs. no inclusivas requisitos. Un _A y Los sufijos _e se utilizan para denotar requisitos universales (todos) frente a requisitos existenciales (existen). Las ventanas de tiempo exacto se indican mediante [n] y flexible por [m..n] .
Operadores de estilo SERE
El operador PSL más utilizado es el operador "sufijo-implicación" (también conocido como el operador "desencadenantes"), 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 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 debería satisfacer la propiedad p. Esto se ejemplifica en las figuras de la derecha.
Las expresiones regulares de PSL tienen los operadores comunes para la concatenación ( ; ), Cierre de Kleene ( * ) y unión ( | ), así como operador de fusión ( : ), Intersección ( \ & \ & ) y una versión más débil ( \ & ), y muchas variaciones para conteos consecutivos [* n] y recuento in-consecutivo p. ej. [= n] y [-> n] .
El operador de gatillo viene en varias variaciones, que se muestran en la tabla a continuación.
Aquí s y t son expresiones regulares de PSL, y p es una fórmula de PSL.
s | => t! | si hay una coincidencia de s, entonces hay una coincidencia de t en el sufijo de la traza,
|
s | -> t! | si hay una coincidencia de s, entonces hay una coincidencia de t en el sufijo de la traza,
|
s | => t | si hay una coincidencia de s, entonces hay una coincidencia de t en el sufijo de la traza,
|
s | -> t | si hay una coincidencia de s, entonces hay una coincidencia de t en el sufijo de la traza,
|
Los operadores para concatenación, fusión, unión, intersección y sus variaciones se muestran en la siguiente tabla.
Aquí s y t son expresiones regulares PSL.
s ; t | coincidencia de s seguida de una coincidencia de t, t comienza el ciclo después de que termina s |
s : t | coincidencia de s seguida de una coincidencia de t, t comienza el mismo ciclo que s termina |
s | t | coincidencia de s o coincidencia de t |
s && t | coincidencia de sy coincidencia de t, la duración de ambos es de la misma longitud |
s & t | coincidencia de s y coincidencia de t, las coincidencias de duración pueden ser diferentes |
s within t | coincidencia de s dentro de una coincidencia de t, abreviatura de ([*]; s; [*]) && (t) |
Los operadores para repeticiones consecutivas se muestran en la siguiente tabla.
Aquí s es una expresión regular de PSL.
s[*i] | i repeticiones consecutivas de s |
s[*i..j] | entre i a j repeticiones consecutivas de s |
s[*i..] | al menos i a repeticiones consecutivas de s |
s[*] | cero o más repeticiones consecutivas de s |
s[+] | una o más repeticiones consecutivas de s |
Los operadores para repeticiones no consecutivas se muestran en la siguiente tabla.
Aquí b es cualquier expresión booleana de PSL.
b[=i] | i no necesariamente repeticiones consecutivas de b,
|
b[=i..j] | al menos iy no más de j no necesariamente repeticiones consecutivas de b,
|
b[=i..] | al menos no necesariamente repeticiones consecutivas de b,
|
b[->m] | m no necesariamente repeticiones consecutivas de b que terminan en b,
|
b[->m:n] | al menos my no más de n no necesariamente repeticiones consecutivas de b que terminan en b,
|
b[->m..] | al menos m no necesariamente repeticiones consecutivas de b que terminan en b,
|
b[->] | atajo para b [-> 1],
|
Operadores de estilo LTL
A continuación se muestra una muestra de algunos operadores de PSL de estilo LTL.
Aquí p y q son fórmulas de PSL.
always p | la propiedad p se mantiene en cada punto de tiempo |
never p | la propiedad p no se mantiene en ningún momento |
eventually! p | existe un punto de tiempo futuro donde p se mantiene |
next! p | existe un próximo punto de tiempo, y p se mantiene en este punto |
next p | si existe un próximo punto de tiempo, entonces p se mantiene en este punto |
next![n] p | existe un n-ésimo punto de tiempo, y p se mantiene en este punto |
next[n] p | si existe un n-ésimo punto de tiempo, entonces p se mantiene en este punto |
next_e![m..n] p | existe un punto de tiempo, entre m-ésimo y n-ésimo desde la corriente donde p se mantiene. |
next_e[m..n] p | si existe al menos n-ésimo puntos de tiempo, entonces p se mantiene en uno de los m-ésimo a n-ésimo puntos. |
next_a![m..n] p | existen al menos n puntos de tiempo más yp se mantiene en todos los puntos de tiempo entre el mes y el enésimo, inclusive. |
next_a[m..n] p | p se mantiene en todos los puntos de tiempo siguientes del mes al enésimo, sin embargo, existen muchos |
p until! q | existe un punto de tiempo donde q se mantiene, yp se mantiene hasta ese punto de tiempo |
p until q | p se mantiene hasta un momento en el que q se mantiene, si existe |
p until!_ q | existe un punto de tiempo donde q se mantiene, yp se mantiene hasta ese punto de tiempo y en ese punto de tiempo |
p until_ q | p se mantiene hasta un punto de tiempo en el que q se mantiene, y en ese punto de tiempo, si existe |
p before! q | p se cumple estrictamente antes del punto de tiempo donde q se cumple, y p finalmente se mantiene |
p before q | p se cumple estrictamente antes del punto de tiempo donde q se cumple, si p nunca se cumple, entonces tampoco q |
p before!_ q | p se mantiene antes o en el mismo punto de tiempo donde q se mantiene, y p finalmente se mantiene |
p before_ q | p se cumple antes o en el mismo punto de tiempo donde q se cumple, si p nunca se cumple, entonces tampoco q |
Operador de muestreo
A veces es deseable cambiar la definición del próximo punto de tiempo , por ejemplo, en diseños de reloj múltiple, o cuando se desea un mayor nivel de abstracción. El operador de muestreo (también conocido como el operador del reloj ), denotado @ , se utiliza para este propósito. La formula p @ c donde p es una fórmula de PSL y c una expresión booleana de PSL se mantiene en una ruta dada si p en ese camino proyectado sobre los ciclos en los que c se sostiene, como se ejemplifica en las figuras de la derecha.
La primera propiedad establece que "cada solicitud que es seguida inmediatamente por una señal de confirmación , debe ir seguida de una transferencia de datos , donde una transferencia de datos completa es una secuencia que comienza con la señal comenzar , terminar con señal final en el cual los datos deben contener al menos 8 veces:
((verdadero [*]; req; ack) | => (inicio; datos [= 8]; final)
Pero a veces se desea considerar solo los casos en los que las señales anteriores ocurren en un ciclo donde clk es alto. Esto se representa en la segunda figura en la que, aunque la fórmula
((verdadero [*]; req; ack) | => (inicio; datos [* 3]; final) @ clk
usos datos [* 3] y [* n] es una repetición consecutiva, la traza coincidente tiene 3 puntos de tiempo no consecutivos donde los datos se mantienen, pero al considerar solo los puntos de tiempo en los que clk se mantiene, los puntos de tiempo donde la retención de datos se vuelve consecutiva.
La semántica de las fórmulas con @ anidada es un poco sutil. Se remite al lector interesado a [2].
Operadores de aborto
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 del modelo acotado, 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 truncada propuesta en [1].
Aquí p es cualquier fórmula de PSL y b es cualquier expresión booleana de PSL.
p async_abort b | p se mantiene op no falla hasta que b se cumple;
|
p sync_abort b | p se mantiene op no falla hasta que b se cumple;
|
p abort b | equivalente ap async_abort b |
Poder expresivo
PSL subsume la LTL lógica temporal y extiende su poder expresivo al de los lenguajes omega-regulares . El aumento en el poder expresivo, en comparación con el de LTL, que tiene el poder expresivo de las expresiones regulares ω sin estrellas, se puede atribuir al sufijo implicación , también conocido como operador de disparadores , denotado "| ->". La fórmula r | -> f donde r es una expresión regular yf es una fórmula lógica temporal se cumple en un cálculo w si cualquier prefijo de w que coincide con r tiene una continuación que satisface f . Otros operadores de PSL que no son LTL son el operador @ , para especificar diseños de reloj múltiple, los operadores de aborto , para tratar con restablecimientos de hardware y las variables locales para la concisión.
Capas
El PSL se define en 4 capas: la capa booleana , la capa temporal , la capa de modelado y la capa de verificación .
- La capa booleana se utiliza para describir un estado actual del diseño y se redacta utilizando uno de los HDL mencionados anteriormente.
- La capa temporal consta de los operadores temporales que se utilizan para describir escenarios que se extienden a lo largo del tiempo (posiblemente en un número ilimitado de unidades de tiempo).
- La capa de modelado se puede utilizar para describir máquinas de estado auxiliares de manera procedimental.
- La capa de verificación consta de directivas para una herramienta de verificación (por ejemplo, para afirmar que una propiedad determinada es correcta o suponer que un determinado conjunto de propiedades es correcto al verificar otro conjunto de propiedades).
Compatibilidad de idiomas
El lenguaje de especificación de propiedades se puede utilizar con varios lenguajes de diseño de sistemas electrónicos (HDL) como:
- VHDL (IEEE 1076)
- Verilog (IEEE 1364)
- SystemVerilog (IEEE 1800)
- SystemC (IEEE 1666) por Open SystemC Initiative (OSCI) .
Cuando PSL se usa junto con uno de los HDL anteriores, su capa booleana usa los operadores del HDL respectivo.
Referencias
- 1850-2005 - Estándar IEEE para lenguaje de especificación de propiedades (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): Estándar para lenguaje de especificación de propiedades (PSL) . 2007. doi : 10.1109 / IEEESTD.2007.4408637 . ISBN 978-0-7381-5727-6.
- 1850-2010 - Estándar IEEE para lenguaje de especificación de propiedades (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): Estándar para lenguaje de especificación de propiedades (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). "Razonamiento con lógica temporal en caminos truncados" (PDF) . Verificación asistida por computadora . Apuntes de conferencias en Ciencias de la Computación. 2725 . pag. 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). "La definición de un operador de reloj temporal" (PDF) . Autómatas, lenguajes y programación . Apuntes de conferencias en Ciencias de la Computación. 2719 . pag. 857. doi : 10.1007 / 3-540-45061-0_67 . ISBN 978-3-540-40493-4.
enlaces externos
- Grupo de trabajo IEEE 1850
- Anuncio de IEEE septiembre de 2005
- Accellera
- Tutorial de lenguaje de especificación de propiedades
- Guía de diseñadores para PSL