Lenguaje de especificación de propiedades

El operador PSL más utilizado es el operador de "implicación de sufijo" (también conocido como 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 instante i tal que la secuencia de instantes hasta i coincide 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 los operadores comunes para concatenación ( ; ), cierre de Kleene ( * ) y unión ( | ), así como el operador 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 disparo se presenta en varias variantes, que se muestran en la tabla a continuación.

Aquí , s y t son expresiones regulares PSL, y p es una fórmula PSL.

En la tabla siguiente se muestran los operadores de concatenación, fusión, unión, intersección y sus variaciones.

Aquí , s y t son expresiones regulares PSL.

Los operadores para repeticiones consecutivas se muestran en la tabla a continuación.

Aquí s es una expresión regular PSL.

Los operadores para repeticiones no consecutivas se muestran en la tabla a continuación.

Aquí b es cualquier expresión booleana de PSL.

A continuación se muestra una muestra de algunos operadores de PSL de estilo LTL (carga parcial).

Aquí p y q son cualquier fórmula 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 mayor nivel de abstracción. 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 se proyecta sobre los ciclos en los que se cumple c , como se ejemplifica en las figuras de la derecha.

La primera propiedad establece que "cada solicitud que sea seguida inmediatamente por una señal de acuse de recibo , debe ir seguida de una transferencia de datos completa , donde una transferencia de datos completa es una secuencia que comienza con la señal de inicio y termina con la señal de fin , en la que los datos deben permanecer al menos 8 veces:

 (verdadero[*]; solicitud; confirmación) |=> (inicio; datos[=8]; fin) 

Pero a veces se desea considerar solo los casos en los que las señales anteriores ocurren en un ciclo donde clk está alto. Esto se muestra en la segunda figura en la que, aunque la fórmula

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

usa data[*3] y [*n] es repetición consecutiva, el rastro coincidente tiene 3 puntos de tiempo no consecutivos donde data se mantiene, pero cuando se consideran solo los puntos de tiempo donde clk se mantiene, los puntos de tiempo donde data se mantiene se vuelven consecutivos.

La semántica de las fórmulas con @ anidado es un tanto sutil. Para más información, consulte [2].

PSL dispone de varios operadores para gestionar rutas truncadas (rutas finitas que pueden corresponder a un prefijo del cálculo). Las rutas truncadas se producen en la verificación de modelos acotados, debido a reinicios y en muchos otros escenarios. Los operadores de aborto especifican cómo deben gestionarse las eventualidades cuando una ruta se ha truncado. Se basan en la semántica de truncamiento propuesta en [1].

Aquí, p es cualquier fórmula PSL y b es cualquier expresión booleana PSL.

PSL engloba la lógica temporal LTL 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 posee el poder expresivo de las expresiones ω-regulares sin estrella, puede atribuirse a la implicación de sufijo , también conocida como operador de activación , denotada "|->". 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 manejar 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 .

• La capa booleana se utiliza para describir el estado actual del diseño y se formula utilizando uno de los lenguajes de descripción de hardware (HDL) mencionados anteriormente.
• La capa temporal consta de los operadores temporales utilizados para describir escenarios que se extienden a lo largo del tiempo (posiblemente durante un número ilimitado de unidades de tiempo).
• La capa de modelado se puede utilizar para describir máquinas de estados 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 para asumir que un conjunto determinado de propiedades es correcto al verificar otro conjunto de propiedades).

El lenguaje de especificación de propiedades se puede utilizar con varios lenguajes de diseño de sistemas electrónicos (HDL), tales como:

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

Cuando se utiliza PSL junto con uno de los lenguajes de descripción de hardware (HDL) mencionados anteriormente, su capa booleana utiliza los operadores del HDL correspondiente.

• Uso de PSL/Sugar para la verificación formal y dinámica, 2.ª edición, Ben Cohen, Ajeetha Kumari, Srinivasan Venkataramanan
• Introducción práctica al PSL , Cindy Eisner y Dana Fisman