| Revista: | Journal of applied research and technology |
| Base de datos: | PERIÓDICA |
| Número de sistema: | 000365924 |
| ISSN: | 1665-6423 |
| Autores: | Torres, D1 Cortéz, J2 González, R. E1 |
| Instituciones: | 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 |
| Año: | 2009 |
| Periodo: | Abr |
| Volumen: | 7 |
| Número: | 1 |
| Paginación: | 15-40 |
| País: | México |
| Idioma: | Inglés |
| Tipo de documento: | Artículo |
| Enfoque: | Experimental, aplicado |
| Resumen en español | 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 |
| Resumen en inglés | 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 |
| Disciplinas: | Ingeniería, Ciencias de la computación |
| Palabras clave: | 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 |
| Texto completo: | Texto completo (Ver HTML) |
