Formale Verifikation mit OneSpin 360 MV erzwingt die 100%-Prüfung

Anbieter zum Thema

MES Electronic Connect GmbH & Co. KG

Cadlog Group

IBR Leiterplatten GmbH & Co. KG

Melexis GmbH

Die Konsequenzen

Beim näheren Betrachten der Situation wäre das Haare raufen ganzer Entwicklungsteams noch das geringste Übel, aber solange unser Problem nicht aufgeklärt und beseitigt wird, werden Tag für Tag weitere dieser Schaltkreise (in Fahrzeugen verbaut) das Werk verlassen. Als schließlich die Untersuchung der Reklamation vom Chiphersteller ergebnislos abgebrochen werden muss, weil der vorerst letzte Proband eines gewaltsamen Todes starb, sind inzwischen schon Monate verstrichen und jeder in der Verarbeitungskette hat einen immensen Aufwand zur Aufklärung des Problems betrieben. Und immer noch ist nicht gänzlich klar, worin das Problem besteht.

Nicht ohne Grund sind Automobilhersteller inzwischen sehr daran interessiert, diese Zuliefererkette einzukürzen und selbst Silizium-Fabrikanten mit ins Boot zu nehmen, um ein Problem möglichst schnell zu adressieren und aufzuklären. Denn die Zeit läuft, und der Gedanke daran, die Fahrzeugflotte einer kompletten Jahresproduktion mit Chips auszurüsten, die möglicherweise einen systematischen Fehler beinhalten könnten, ist eine der schlimmsten Vorstellungen überhaupt. Vor diesem Hintergrund erscheint selbst eine ESD-Schwäche eher harmlos, zwar unangenehm, aber wenigstens klar sichtbar und handhabbar, einmal erkannt meist mit wenig Zeitaufwand und Risiko zu beseitigen. Die immensen Kosten, die im Gegensatz dazu in unklare Reklamationen gesteckt werden, sind das eine, jedoch ist die Zeit, die es benötigt, den Fehler zu finden und abzustellen das eigentlich ärgerliche daran. Die drohenden Kosten für eventuell notwendig werdende Rückrufaktionen vor Augen muss schnell gehandelt werden.

Auf der Suche nach etwas, von dem man nicht weiß, was es ist

Noch sind wir dem Problem nicht viel näher gekommen. Der bisher einzige Fortschritt ist eher mentaler Art, wir akzeptieren inzwischen die Möglichkeit eines unbekannten Bugs. Bloß wie finden wir etwas, das wir nicht einmal genau beschreiben können?

Nach der Strategie von Sherlock Holmes gedacht, muss unser Fehler konsequenterweise genau dort sein, wo wir unvollständig oder gar nicht simuliert haben. Nur hilft uns das in diesem Fall nicht viel weiter. Die unglaubliche Zahl von 2hochN digitalen Zuständen macht jeden Versuch einer vollständigen Simulation aller Kombinationen von vornherein aussichtslos, zu komplex ist der Chip – und es wäre reiner Zufall, auf diese Weise auf den Bug zu stoßen. Und selbst würde dieser unglaubliche Zufall tatsächlich eintreten, wer garantiert, dass es der einzige Bug ist?

Erinnern wir uns noch einmal: richtig oder falsch und nicht so „ungefähr“ kann ein Digitalschaltung arbeiten – und dass dieses ein Vorteil ist. Auf der Suche nach Begriffen wie „Vollständigkeit“, „Verifikation“, „mathematisch“ und „beweisen“ stößt man unweigerlich auf etwas, was genau dem entspricht was wir jetzt brauchen, den vollständigen mathematischen Nachweis aller spezifizierten Funktionen X und im Gegenzug, dem Ausschluss aller restlichen 2hochN-X möglichen Zustände mit der Aussage, dass diese keine unerwünschten Verhaltensweisen verursachen. Nur wenn wir beide Antworten wissen, können wir sicher sein, dass alle Funktionen richtig entworfen wurden.

OneSpin 360 MV – mathematischer Nachweis der Richtigkeit

Inzwischen ist klar geworden, es genügt uns nicht zu wissen, dass der Chip die spezifizierten Funktionen erfüllen wird. Der Schlüssel zum Erfolg liegt zukünftig darin, jegliche mögliche Verhaltensweise eines digitalen Zustandsraumes mathematisch als korrekt zu beweisen. Leistungsstarke Tools wie 360 MV von OneSpin Solutions treten den Kampf gegen die Verifikationslücke an und das wirklich tolle daran ist – es gelingt tatsächlich diese bisher industriell nie erreichbare 100%-Vollständigkeit der Verifikation zu erzwingen und damit endlich mathematisch zu beweisen, was mit anderen Verifikationsansätzen unmöglich geworden ist.

Der Erfolg der Methoden der formalen Verifikation gründet sich nicht unwesentlich auf die damit erzielbare und garantierbare mathematische Vollständigkeit. Der Firma OneSpin Solutions ist es gelungen, nicht nur leistungsstarke Algorithmen zur funktionalen Verifikation von digitalen Schaltungen zu implementieren. Das Tool 360 MV bietet darüber hinaus eine einzigartige automatische Abdeckungsanalyse, ob auch wirklich alle Verifikationslücken geschlossen wurden, also jedwede Designfunktionalität inklusive aller selten vorkommenden Randverhalten vollständig verifiziert ist.

Diese Analysen liefern detaillierte Informationen, wo es im RTL-Code Abweichungen zum spezifizierten Verhalten gibt und darüber hinaus, wo Verifikationslücken bestehen. Dies ist umso wichtiger, da das reine Wissen um einen möglichen Bug und um Verifikationslücken erst dann wirksam wird, wenn die betreffenden Stellen möglichst schnell und effektiv im Code gefunden werden. Besonders im Fokus sind scheinbare Randfunktionen der Spezifikation, Funktionen die selten oder fast nie gebraucht werden, denn entsprechend spät im Verlauf einer Produktentwicklung kommt es zu einer Aufdeckung darin verborgener Fehler und die Behebung betrifft damit bereits nicht mehr nur den Chiphersteller selbst, sondern auch die Zulieferer bis sogar hin zum Endanwender.

Diese komplette Analysefunktionalität ist eines der herausragenden Ergebnisse des durch das BMFT geförderten Projektes Herkules. So unterstützt das Verifikationstool 360 MV durch Aussagen über den aktuellen Grad der Verifikation und die Überwachung der Gültigkeit der Verifikation nach vorgenommenen Korrekturen am Design die Sicherheit der Projektplanung. Wunderbar ist hieran: Der verbleibende Aufwand bis zur Vollständigkeit kann durch die automatische Abdeckungsanalyse als linear betrachtet werden, wohingegen der Zuwachs einer Simulationsabdeckung eher einer e-Funktion folgt und oberhalb von 80% nur mit immer größerem Aufwand immer kleiner werdende Fortschritte macht, ohne jemals die 100% erreichen zu können.

Der Grund liegt in der verschiedenen Herangehensweisen begründet. Jede weitere Simulation beinhaltet zwangsläufig einen großen Anteil bereits schon einmal verifizierter Schritte. Die cleveren Algorithmen der formalen Abdeckungsanalyse konzentrieren sich ausschließlich auf die Identifikation von Verifikationslücken und geben Informationen aus, wo noch nicht hundert Prozent erreicht sind und warum. Betrachtet man das zuvor beschriebene und der Praxis entnommenen Beispiel eines realen System-Chips, wird klar: In naher Zukunft wird diese neue Qualität der Verifikation ein unbedingtes „Muss“ sein. Rasant steigende Herstellungskosten für Masken und der hohe Aufwand für Fehleranalysen und für jedes noch so kleine Re-Design lassen es nicht mehr zu, das Risiko solcher „versteckten“ Bugs bis zum Endanwender zu verschleppen.

Kooperation von OneSpin Solutions und Melexis

Im Rahmen der BMBF-Förderprojekte VALSE, VALSE-XT, und HERKULES wurde in den letzten Jahren intensiv an Methoden der formalen Verifikation gearbeitet, um die so dringend benötigten Werkzeuge zur Schließung der Verifikationslücke derart leistungsfähig zu machen, dass sie den rasant steigenden Anforderungen der Praxis standhalten. Neben Alcatel-Lucent, Infineon, Bosch, Siemens, weiteren bekannten Halbleiterherstellern sowie in Zusammenarbeit mit deren Kooperationspartnern an Hochschulen und Instituten war auch die Firma Melexis an der methodischen Erarbeitung beteiligt und ist hochmotiviert, diese neuen und den Erfolg ihrer Entwicklungen sichernden Tools anzuwenden. Melexis entwickelt und produziert eine breite Palette von Mixed-Signal-Hochvolt-ASIC (Application Specific Integrated Circuit) und ASSP (Application Specific Standard Product), in zunehmendem Maße mit integriertem Flash und Mikrocontroller(n), LIN physical Layer oder komplettem LIN Controller, CAN für Automobilanwendungen.

Die Zeichen der Zeit erkennend, nutzt Melexis die Methoden der formalen Verifikation insbesondere an den Brennpunkten der Entwicklung im Designflow. Die Verwertung der gewonnenen Kenntnisse wird direkt in die zukünftigen Melexis-IP-Entwicklungen eingehen, um deren Fehlerfreiheit bereits während des Entwurfsprozesses und damit möglichst frühzeitig sicherzustellen. Die Fehlerfreiheit der IP ist für den Erfolg der damit entwickelten Produkte von strategischer Bedeutung.

Neue Methoden der kombinierten Verifikation

Während der Forschungsarbeiten wurden durch Melexis neue Methoden für die kombinierte Verifikation von Hardware und Software an einem Demonstrator mit LIN Komponenten entwickelt. Dabei wurde an einem der eingesetzten Mikroprozessor-IP überraschenderweise nicht-spezifikationskonformes Verhalten gefunden, das sich bisher nie in der Praxis ausgewirkt hatte. Vorsorglich wird dieser Befehl im Compiler gesperrt, um damit potenzielle Probleme garantiert auszuschließen. Solche versteckten und bis dato unbekannte Schwächen lassen sich nur noch mit formaler Verifikation sicher finden und mit deren Beseitigung (oder wie in diesem Fall dem Ausschluss der Funktion im Compiler) kann der immense Aufwand zur Aufklärung „sporadischer Fehlfunktionen“ verhindert werden.

An dem von der Firma Melexis entwickelten LIN-Demonstrator wird gezeigt, dass diese neuen Methoden auch in der Lage sind, die Verifikation von Software (in dem Fall die Protokoll-Software eines LIN-Slaves) in Kombination mit der LIN Physical Layer vorzunehmen. Dieses senkt das Risiko, mit Updates und Re-Designs das Einbringen neuer Fehler in schon bestehende Applikation zu riskieren. Wie leicht einzusehen ist, birgt der immer stärkere Einsatz von IP-Blöcken neben den Vorteilen einer schnellen Verfügbarkeit und der Reduzierung des Aufwandes bei der Entwicklung eines Chips auch eine neue Gefahr, mögliche noch unentdeckte Bugs in eine Vielzahl von Entwicklungsprojekten zu übertragen, die diese IP nutzen.

Re-using ist das probate Mittel die Entwicklungszeiten zu verkürzen und trotzdem immer höher integrierte IC zu entwerfen. Daher ist es unabdingbar, dass solche IP fehlerfrei funktionieren. Die vereinfachte Betrachtung der Verifikationsqualität eines simulierten IP (nehmen wir eine Abdeckung von 90% pro IP an) lässt schnell erkennen, dass die sich aus der Multiplikation ergebende Gesamtqualität eines späteren ICs mit der Anzahl solcher eingesetzter 90%-IP drastisch sinken muss. Die Wahrscheinlichkeit, dass der Chip die Spezifikation einhält, sinkt mit jedem weiteren solchen IP, der nicht 100% verifiziert ist. Nur durch eine vollständige Verifikation jeder einzelnen Komponente lässt sich dieser simplen Tatsache entgegenwirken.

Höchste Qualität ist ein Muss

Für Melexis mit ihrer Produktpalette aus ASIC und ASSP ist der Anspruch an eine höchstmögliche Qualität und die Einhaltung von Entwicklungszeiten zur Sicherung der Zufriedenheit ihrer Kunden unabdingbar. Dies lässt sich nur dadurch erreichen, dass alle Möglichkeiten ausgeschöpft werden, um Risiken auszuschließen, die sich aus einer unvollständig gebliebenen Verifikation während einer Entwicklung ergäben. Selbst die intensivste Erprobung ist dem gleichen Dilemma wie eine Simulation unterworfen. Auch die Erprobung kann nicht 100%-ig erfolgen, wirkt allerdings aus Sicht der Überdeckung ergänzend zu der einer Simulation. Erprobung hat den Nachteil, dass erst dort gefundenen Fehler eine Neuprozessierung der Wafer erfordern.

In der Auswertung von Redesign- Gründen aus Entwicklungen der vergangenen Jahre wird deutlich, dass Bugs viel zu oft simple digitale Fehler sind, die sich nur dadurch einer sofortigen Entdeckung entziehen konnten, weil sie in der hohen Komplexität untergingen. In etwa 60% der Re-Designs wurden digitale Fehler mit unterschiedlichem Grad einer Funktionsstörung korrigiert. So ist der Fokus auf den Digitalteil und dem Erlangen des mathematischen Beweises, dass zumindest auf dem hochintegrierten Teil des Siliziums keine Entwurfsfehler existieren, mehr als berechtigt. Die komplette Fehlerfreiheit des Digitalteiles reduziert angenehmerweise auch drastisch den Aufwand bei der Verifikation des Gesamtsystems, wenn man bereits auf den gesamten Digitalteil vertrauen kann und nicht jede einzelne Grundfunktion mit langen Rechenzeiten bestätigen muss.

Es ist sicher nachvollziehbar wie ärgerlich es ist, wenn der Erfolg stundenlanger Simulationen durch das Entdecken eines simplen vergessenen Inverters zunichte gemacht wird. Formale Verifikation eröffnet die Möglichkeit die für die Kunden notwendige Qualität und Planungssicherheit auch versprechen zu können und ist ein wichtiger Baustein zur Sicherung des Entwicklungserfolges. Letztlich ist der Aspekt der Produktgewährleistung auch für SOC-Entwicklungen zu beachten. Gut beraten ist, wer solche Aussagen beweisen kann und nicht nur verspricht, alles getan zu haben, was dem aktuellen Stand der Technik entspricht.

Die Welt ist auch weiterhin analog

Die Methoden formaler Verifikation sind nicht zwangsläufig auf die Welt digitaler Schaltungen beschränkt, auch wenn in ihren Ursprüngen genau diese Domäne der Auslöser dafür war, sie zu entwickeln. Der rechnerische Beweis von Korrektheit lässt sich für jedes System erzielen (Verilog HDL, VHDL auf RTL oder digitalen Netzlisten), das mit Booleschen Gleichungen beschreibbar ist. Im Rahmen der Förderung durch das BMBF (Förderkennzeichen VALSE: 01M3052, VALSE-XT: 01M0369, HERKULES: 01M3082) ist es der Firma Melexis gelungen, methodisch auch Bereiche des analogen Umfeldes eines Digitalteils zu erschließen, die sich prinzipiell durch eine Modellierung einbeziehen lassen. Und sei es durch einen Trick der Digitalisierung analoger Signale. Wie alle guten Ideen erscheint es naheliegend, man muss eben nur darauf kommen.

Ein typisches Beispiel ist ein ADC-Signalpfad mit Verstärkern, Multiplexern und dem ADC selbst. Es ist bei der Einbeziehung solcher Komponenten erklärtermaßen nicht das Ziel, diese analogen IP per formaler Verifikation zu verifizieren, sondern die Vorgehensweise soll dazu dienen, die bis dahin nicht einfach zu beantwortende Frage nach der korrekten Einbindung des Digitalteils zu beantworten und den hohen Rechenaufwand einer Mixed-Signal-Simulation zu reduzieren.

Diese Ersatzmodellierung ist insofern zulässig, weil solche analogen Komponenten aus analogen Standardbibliotheken stammen, deren Korrektheit mehrfach in der Praxis bewiesen wurde. Schon eine simple Abdeckung aller Signalkombinationen an der Schnittstelle zwischen digitalem Kern und analogen Komponenten ist per Mixed-Signal-Simulation kaum noch zeitnah möglich. Zumindest lässt sich aber mit leistungsfähigen Methoden erreichen, dass eine Aussage über potenzielle logische Fehler an einer Schnittstelle deutlich besser getroffen werden kann.

Ein weites Feld der kreativen Betätigung für Verifikationsspezialisten wird in wachsendem Maße die Verifikation von Soft-Macros. Solche Macros kommen oft dann zum Einsatz, wenn über die Produktlebensdauer damit gerechnet werden muss, dass es Spezifikationsänderungen geben wird. Typische Beispiele sind Protokoll-Schnittstellen. Weit verbreitet sind im automotiven Einsatz der LIN (Local Interconnect Network), CAN (Controller Area Network), SPI (Serial Peripheral Interface) und SENT (Single Edge Nibble Transmission). Aus Sicht des Anwenders betrachtet sind solche Funktionen reine Hardware-Makros, die er in seiner Anwendersoftware nutzt, auch wenn sich dahinter oft kleine Prozessoren verbergen – mit eigener Software und eigenem Speicher. Wie die Fehlerfreiheit dieser Makros inklusive ihrer Software zu beweisen ist, insbesondere vor Software-Updates, wurde im Verlauf des Förderprojektes HERKULES durch Melexis methodisch aufbereitet.

Für die Welt der Mixed-Signal-Schaltkreise ist formale Verifikation kein Allheilmittel, aber ein großer Schritt in die richtige Richtung, sich den steigenden Anforderungen zu stellen. Insbesondere für die Verifikation von digitalen Blöcken ist sie eine effiziente Alternative zur Simulation auf Blockebene; eine Alternative, die wesentlich höhere Qualität sicherstellt. In Kombination mit simulativen Verfahren auf Systemebene entlastet in solchen Entwicklungen der mathematische Ausschluss von Fehlern im Digitalteil die Gesamtsystemverifikation erheblich durch den zusätzlichen Effekt, dass sich diese Simulationen wiederum auf die Überprüfung der elektrischen Korrektheit wie Biasing, Ströme, Supply-System, ESD-Verhalten, Referenzen, Parameter und deren Genauigkeiten u.v.a. auf Systemebene konzentrieren können.

Es sind nicht nur die Digital-Megachips, die vom Einsatz der formalen Verifikation profitieren. Selbst für die im Vergleich mit anderen Herstellern eher kleine Firma Melexis ist formale Verifikation gewinnbringend auch für Mixed-Signal-Schaltkreis-Entwicklungen einsetzbar, steigert sich doch die Qualität ihrer Schaltkreise und sichert somit den Erfolg der Melexis-Produkte am Markt. Jubeln darf, wer bereits jetzt einen Stempel auf seine Dokumente bringen könnte, der vielleicht bald heißt: „Certified by Formal Verification“. Diese Zertifizierung der Qualität entwickelter Schaltungen und deren funktionale Korrektheit ist ein Schlüssel für den garantierbaren Erfolg zukünftiger Entwicklungen, mit dem ein klares Differenzierungsmerkmal entsteht; ein wichtiger Wettbewerbsvorteil für die Anwender der Methoden der formalen Verifikation.

*Roland Syba ist Entwicklungsingenieur bei Melexis in Erfurt.

(ID:356648)