Die schnelle Entwicklung der VLSI-Technologie zwingt die Hersteller, immer komplexere Schaltkreise in k?zerer Zeit herzustellen. Dazu wird es immer wichtiger nachzuweisen, dass die neuen Schaltkreise logisch korrekt sind.

Das Zentrale Forschungslaboratorium von Siemens hat ein Schaltkreis-Verifakations-System (CVE) entwickelt, das auf neuartigen Prinzipien beruht. CVE berechnet das Ausgabe-Verhalten eines digitalen Schaltkreises als boolesche Funktion von diessen Eingaben. Sequentielle Schaltkreise werden als endliche Automaten betrachtet. Die berechneten Funktionen werden symbolisch mit den entsprechenden Funktionen der formalen Spezifikation des Schaltkreises vergleichen, wobei spezielle, effiziente Algorithmen verwendet werden, die gew?rleisten, da"s alle Abweichungen entdeckt werden.

CVE garantiet 100-prozentige Sicherheit, da der symbolische Vergleich ?uivalent ist einer Simulation des Schaltkreises mit allen m?lichen Eingabe- und Ausgaben.

CVE ist in IF/Prolog V5.0 mit Constraints und C implementiert.

scroll to top