Semi-formal specifications and formal verification improving the digital design: some statistics



Document title: Semi-formal specifications and formal verification improving the digital design: some statistics
Journal: Journal of applied research and technology
Database: PERIÓDICA
System number: 000365924
ISSN: 1665-6423
Authors: 1
2
1
Institutions: 1Instituto Politécnico Nacional, Centro de Investigación y de Estudios Avanzados, México, Distrito Federal. México
2Instituto Tecnológico de Sonora, Ciudad Obregón, Sonora. México
Year:
Season: Abr
Volumen: 7
Number: 1
Pages: 15-40
Country: México
Language: Inglés
Document type: Artículo
Approach: Experimental, aplicado
Spanish abstract En el presente trabajo se propone una mejora a la metodología del ciclo de diseño digital tradicional. La contribución principal es la generación de un conjunto de propiedades a partir de una especificación semi–formal de requerimientos, que permiten la verificación formal automática de una máquina de estados finitos (FSM). Estas propiedades se escriben en el lenguaje PSL. Se muestra cómo, a partir de las propiedades, se puede obtener código VHDL que implementa la máquina de estados. Nuestros resultados muestran que la metodología de diseño propuesta resulta en una disminución del tiempo requerido para realizar la verificación
English abstract In this work, an improvement of the traditional digital design methodology is proposed. The major change is the use of a semi–formal specification for the code implementation, the use of a verification tool and the establishment of properties for the formal verification of Finite State Machines (FSM). From semi–formal specifications, assertions were written using Property Specification Language (PSL) for an alignment circuit. Finally, a set of properties for the verification of this module were established and proved using a model checking tool. Our statistics proved that the whole design process was improved and considerable design time was saved
Disciplines: Ingeniería,
Ciencias de la computación
Keyword: Ingeniería de control,
Maquinas de estado finito,
Especificación semi-formal,
Verificación formal
Keyword: Engineering,
Computer science,
Control engineering,
Finite state machines,
Semi-formal specification,
Formal verification
Full text: Texto completo (Ver HTML)