Generación de vectores para la verificación de circuitos booleanos mediante MILP

Abstract

Este Proyecto Fin de Carrera presenta una metodología para la generación de vectores de verificación basada en Programación Lineal Entera Mixta. La metodología propuesta da lugar a una herramienta que hace uso de diversos programas desarrollados, en lenguaje de programación C, a lo largo de este PFC y que se ejecutan a nivel de línea de comandos. La herramienta desarrollada permite generar patrones para la verificación en la que se especifican, por ejemplo, el porcentaje de entradas y/o salidas que han de fijarse. Esta herramienta se ha evaluado mediante un banco de pruebas estándar ISCAS’85, empleado extensamente en la bibliografía. Se han escogido de dicho banco de pruebas los circuitos combinacionales más representativos del estado del arte. La complejidad de los mismos va desde unas pocas puertas, C17 con 6 puertas, a circuitos de complejidad media con aproximadamente 3500 puertas como es el caso del C7552. En términos de entradas/salidas, la complejidad alcanza las 233 entradas para el C2670 ó 5 entradas para el C17 y desde las 2 salidas con que cuenta C17 hasta las 140 salidas para C2670 . Todas las pruebas realizadas demuestran la eficiencia de la metodología propuesta y la validez de la herramienta desarrollada. Los tiempos requeridos para obtener los vectores de verificación se encuentran siempre por debajo de 1,5 segundos en todas las pruebas realizadas en este PFC, salvo en contadas ocasiones que se corresponden con el circuito C7552 que requiere aproximadamente 33 segundos. Esa diferencia de tiempos es debida principalmente a la complejidad de interconexión de las puertas de dicho circuito de referencia. Se puede concluir que el desarrollo de este PFC ha logrado satisfactoriamente los objetivos planteados inicialmente, sirviendo como punto de partida de una futura tesis doctoral en base a los resultados obtenidos.

This PFC presents a methodology for the generation of verification patterns using Mixed Integer Linear Programming. Based on proposed methodology, this PFC develops a verification tool made by several programs developed in C programming language. The verification tool is executed at the shell command line interface. The developed tool allows to generate verification patterns which are specified for example with a percentage of inputs and/or outputs to be asserted. This verification tool has been evaluated using ISCAS'85 standard testbenches, widely used in the literature. The most representative combinational circuits of the state of the art have been chosen from testbenches. Their complexity ranges from a few gates, C17 with 6 gates, to medium complexity circuits with approximately 3500 gates as is the case of the C7552. In terms of inputs/outputs, the complexity reaches 233 inputs for the C2670 or 5 inputs for the C17 and from the 2 outputs with C17 up to the 140 outputs for C2670. All tests demonstrate the efficiency and usefulness of the proposed methodology and developed verification tool. The time required to obtain the verification patterns was always less than 1.5 seconds in all tests performed in this PFC. Only for circuit C7552, the required time to obtain the solution rises to approximately 33 seconds. This difference is mainly due to the complexity of its internal interconnection in this reference circuit. It can be concluded that the development of this PFC has satisfactorily achieved the objectives set out initially, serving as a starting point for a future PhD. based on the obtained results.