Symbolic analysis of switch-level circuits

Resumen

La verificacion de circuitos mediante tecnicas simbolicas permite reducir el numero de pasos hacia diseños correctos. Estas mismas tecnicas pueden complementar soluciones convencionales en la generacion y validacion de patrones de test para los circuitos diseñados. En este trabajo se ha creado un entorno matematico que permite el modelado de circuitos a nivel de transistor y asegura la validez de los resultados de algoritmos dirigidos por eventos que se utilizan para analizar los circuitos. En particular, se ha relacionado una algebra booleana de funciones de cuatro valores con la representacion de los caminos electricos desde los nodos de un circuito hasta el de alimentacion y el de tierra. Las dos clases de caminos se representan individualmente a traves de dos funciones definidas en una algebra de dos valores y se obtienen a traves de una simulacion simbolica dirigida por eventos. Finalmente, se ha realizado el programa correspondiente (symsim) y se ofrece una metodologia completa para la comprobacion de estas funciones asociadas a los nodos de los circuitos, asi como una aproximacion a la generacion de vectores de test en la que, ademas, se describe un algoritmo para su compactado.