Resumen de Verificación de circuitos independientes de la velocidad con modelos simbólicos de redes de Petri

Oriol Roig, Enric Pastor, Jordi Cortadella Fortuny

• Este artículo presenta una metodología para verificar circuitos independientes de la velocidad a partir de su especificación descrita mediante redes de Petri. Se utilizan técnicas basadas en análisis simbólico, en las que tanto el circuito como su especificación se modelan como álgebras booleanas, lo que permite enumerar sus estados utilizando funciones booleanas. Estas funciones se representan de forma compacta mediante Diagramas Binarios de Decisión (BDD). Métodos de síntesis basados en STGs pueden ser verificados directamente, ya que utilizan el mismo formalismo que la técnica de verificación aquí presentada. Nuestra metodología ha sido aplicada a varios ejemplos, probando así su utilidad.