Design-Software, EDA -

Formale Verifikation fürs Internet of Things „Fehler aufdecken und Reparaturen vermeiden“

Raik Brinkmann von OneSpin plädiert für die Halbleiterverifikation auch bei kleineren IoT-Bausteinen: Entwicklerteams dürfen dabei keine Abkürzungen nehmen, und formale Tools sind hier durchaus angebracht.

eli: Herr Brinkmann, können Sie uns zunächst etwas über sich und OneSpin Solutions erzählen?

Brinkmann: Gern! Ich bin President und CEO von OneSpin und war Mitbegründer bei der Ausgründung des Unternehmens aus Infineon Technologies in München. Ich bin bereits seit vielen Jahren in der formalen Verifikation tätig und stolz darauf, an der Spitze von OneSpin zu stehen – dem weltweit einzigen Unternehmen, das sich auf Tools für die formale Verifikation von Halbleiterbausteinen spezialisiert hat.

eli: Welche Art von Produkten verifizieren Ihre Kunden mit diesen Tools?

Brinkmann: Unsere Kunden entwickeln Chips in einem breiten Spektrum von Technologien, von FPGAs über ASICs bis zu rein kundenspezifischen Schaltungen, sowie für ein weites Anwendungsfeld. Smartphones und Tablets, Computer, Grafik, Netzwerke, die Telekommunikationsinfrastruktur, Luft- und Raumfahrt und so weiter. Das heißeste Diskussionsthema dürften derzeit Chips für selbstfahrende Autos und andere autonome Fahrzeuge sein. Die Automotive-Elektronik repräsentiert das obere Ende der Anwendungen im Internet of Things, doch einige unserer Kunden entwickeln auch einfachere IoT-Applikationen.

eli: Diese Aussage überrascht mich, denn die formale Verifikation wird häufig als eine fortschrittliche Technologie hauptsächlich für sehr umfangreiche Designs gesehen. Die meisten IoT-Chips sind aber doch eher klein.

Brinkmann: Das stimmt, meist denkt man bei IoT-Bausteinen an billige Massenware, die bei einem Ausfall eher entsorgt als aktualisiert oder repariert wird. Das heiß aber nicht, dass diese Geräte einfach auszutauschen wären. Viele IoT-Bausteine werden an schwer zugänglichen Stellen eingesetzt – denken Sie nur an die Umgebungssensoren in einem Gebäude oder an eine Überwachungskamera, die in großer Höhe an einer Außenwand angebracht ist. Physische Reparaturen können hier sehr teuer sein. Einige Probleme wären vielleicht mit einem Software-Patch zu beheben, aber möglicherweise verbietet sich ein Fernzugriff aus Sicherheitsgründen. Außerdem wissen wir von unseren Handys und Computern, dass ein Softwareupdate möglicherweise einen manuellen Reboot erfordert. Es ist deshalb wirklich am besten, alle Fehler vor dem Deployment eines IoT-Chips aufzudecken, um eine Reparatur oder einen Austausch im Feld zu vermeiden.

eli: IoT-Bausteine können also hohe Verifikationsanforderungen stellen. Sind aber formale Tools hier nicht ein Overkill?

Brinkmann: Keineswegs, zumal viele IoT-Bausteine recht komplex sind. Sehen Sie sich doch einmal die Datenblätter der Atom-Familie von Intel oder die der neuesten ARM-Produkte an. Es gibt da mehrere Prozessorkerne, spezielle Prozessoren, mehrstufige Speichersysteme, anspruchsvolle I/O-Kanäle und so weiter. IoT-Entwicklerteams dürfen bei der Verifikation keine Abkürzungen nehmen, und formale Tools spielen hier eine wichtige Rolle. Ein wesentlicher Aspekt ist außerdem, dass nur die formale Verifikation wirklich Sicherheit bietet. Bei der Simulation und Emulation weiß man nie, wann man mit dem Testen aufhören kann, denn es ist ungewiss, ob es noch unentdeckte Fehler gibt. Formale Tools dagegen finden nicht nur alle Fehler, sondern weisen auch die Sicherheit des Designs nach, wenn keine Fehler mehr gefunden werden können. Wenn Sie wollen, dass Ihre IoT-Bausteine fehlerfrei sind und ihr Leben lang keine Probleme machen, bleibt Ihnen nur die formale Verifikation.

eli: Ist aber die formale Verifikation nicht schwierig anzuwenden und kommen die IoT-Teams mit ihr zurecht?

Brinkmann: Formale Tools sind heute wesentlich einfacher anzuwenden als früher. Wir bieten für gängige Verifikationsprobleme eine breite Palette formaler Apps, also Applikationen, an (mehr dazu im Online-Service, Anmerkung der Redaktion). Diese Apps arbeiten buchstäblich auf Knopfdruck und erreichen eine sehr hohe Rentabilität. Natürlich gibt es einige Arten von Problemen und bestimmte Chiptypen, die eine fundierte Analyse erfordern. Hier können wir aber mit passenden Schulungen und den richtigen Methodiken helfen, zumal unsere Tools mit jedem neuen Release leistungsfähiger und stärker automatisiert werden.

eli: Welche Arten von Fehlern lassen sich mit formalen Tools finden?

Brinkmann: Unsere Apps verifizieren die chipinterne Konnektivität, standardisierte Busprotokolle, Register und Speicher, Scoreboards, Gleitkommaarithmetik und mehr. Sie decken unerreichbaren Code ebenso auf wie nicht genutzte Signale, Fehler in Zustandsautomaten, Unstimmigkeiten zwischen Synthese und Simulation sowie weitere Probleme. Alle diese Kategorien erfordern ein Minimum an Aufwand. Wenn Sie eine gründlichere Analyse wollen, schreiben Sie möglicherweise bestimmte Assertions, um wichtige Aspekte Ihrer Designintention zu erfassen. Dies macht zwar mehr Arbeit, aber wir bieten hierfür Hilfe und Anleitung. Besonders gut ist die fundierte formale Verifikation im Aufdecken grenzwertiger Bugs, die nur beim Zusammentreffen ganz bestimmter Bedingungen auftreten, wie sie in Simulationen nie auftreten würden. Schließlich bietet das formale Equivalence Checking die Gewähr, dass sich beim Modifizieren eines Designs keine Fehler eingeschlichen haben – zum Beispiel durch Logiksynthese, das Einfügen von Teststrukturen oder einen Änderungsauftrag, eine sogenannte Engineering Change Order, ECO.

eli: Es fällt auf, dass der Begriff ‚Safety‘ bei der Chipverifikation häufig benutzt wird. Ist das für IoT-Bausteine relevant?

Brinkmann: Ja, durchaus! Viele Designs müssen Safety-Normen erfüllen, wie die ISO 26262 im Automobilbereich. Diese Normen legen die Messlatte hoch, was die Pre-Silicon-Verifikation angeht – mit einem strukturierten Plan, der Erfassung solider Messwerte und der Zuordnung der Ergebnisse zu den Designfeatures. Ebenso verlangen diese Normen jedoch Sicherheit gegenüber zufälligen Fehlern im Feld, wenn sich das Produkt im Einsatz befindet. Wenn beispielsweise ein Alphateilchen den Zustand eines Bits in einem Ihrer Speicher ändert, sind Sie unter Umständen gefordert, diesen Fehler zu erkennen und möglicherweise sogar zu beheben. Wir haben eine Reihe formaler Apps, die die Auswirkungen zufälliger Fehler nachbilden. Sie analysieren den Umgang Ihres Designs mit diesen Fehlern und dokumentieren die Ergebnisse mit den von den Safety-Normen verlangten Angaben.

eli: Den Nutzen der Unempfindlichkeit gegenüber zufälligen Fehlern kann ich bei selbstfahrenden Autos oder Medizingeräten durchaus nachvollziehen, aber wie ist es im übrigen IoT-Bereich?

Brinkmann: Je mehr Menschen sich auf IoT-Geräte verlassen, umso wichtiger ist deren Betriebssicherheit. Oder möchten Sie, dass ein Alphateilchen die Alarmanlage in Ihrem Haus außer Betrieb setzt, Ihre Eingangstür entriegelt oder Ihr Smartphone funktionsunfähig macht, wenn Sie keinen Festnetzanschluss zum Absetzen eines Notrufs mehr haben? IoT-Geräte mögen zwar klein und unspektakulär erscheinen, sie sind es aber nicht unbedingt. Sie können nicht bei der Verifikation Ihres Chips halbe Sachen machen und dennoch eine einwandfreie Funktion von ihm erwarten.

eli: Einige IoT-Hersteller verwenden FPGAs, damit sie schnell neue Produktgenerationen herausbringen können, ohne die Fertigungszyklen von ASICs abwarten zu müssen. Wird die Arbeit mit FPGAs einfacher?

Brinkmann: Das glaube ich nicht. Die alte Vorgehensweise, ein FPGA im Labor zu debuggen und es nach der Beseitigung aller Fehler umzuprogrammieren, funktioniert bei den heutigen großen SoC-Designs nicht mehr. Ein FPGA-SoC ist in jeder Hinsicht so schwierig zu verifizieren wie jedes andere SoC. Beim Equivalence Checking stellen FPGA-Designs sogar noch höhere Anforderungen als ASICs, was an den aggressiven Optimierungen während des Syntheseprozesses liegt.

eli: Was erwarten Sie, worauf werden sich Elektronikingenieure in Zukunft mehr und mehr einstellen müssen?

Brinkmann: Ich denke, dass systematische Fehler durch systematische Ansätze vermieden werden müssen – beim Design und der Verifikation unter Verwendung kontinuierlicher Fortschrittskontrolle durch Metriken; das Stichwort heißt Coverage. Speziell Standards zur funktionalen Sicherheit verlangen ein solches Vorgehen, um den Entwicklungsprozess nachvollziehbar zu machen. Es ist aber auch grundsätzlich sinnvoll, wenn komplexe Systemchips entwickelt werden, um Projektfortschritt und Kosten unter Kontrolle zu halten. Zudem ist ja allgemein bekannt, dass Fehler teurer sind, je später sie entdeckt werden. Da die SoC-Projekte immer aufwändiger werden, ist neben der Fehlervermeidung auch die frühe Erkennung extrem wichtig. Kontinuierliche Verifikation im Sinne iterativer Entwicklung ist hier ein Schlüsselelement. Formale Techniken sind hier besonders hilfreich, weil sie weniger Aufwand zur Entwicklung der Testumgebung erfordern.

Danke für das Gespräch.

OneSpin Solutions GmbH,
Nymphenburger Straße 20a,
80335 München,
Tel. 089 99013-0,
E-Mail info@onespin.com,
www.onespin.com
Tipps vom Experten: Das Thema Verifikation darf man weder unterschätzen noch unterfinanzieren. Hier sind IoT-Bausteine keine Ausnahme. Sie müssen gründlich arbeiten, um etwaige Bugs vor der Herausgabe eines Designs zu finden und zu beheben, und die Designer müssen die Gewissheit haben, dass das Produkt auch in widrigen Umgebungen sicher arbeitet. Zum Erreichen dieser Ziele bedarf es einer Kombination verschiedener Verifikationsmethodiken, wobei formale Tools an verschiedenen Stellen eine entscheidende Rolle spielen. Raik Brinkmann: „Wir freuen uns, dass die Lösungen von OneSpin hier helfen können, und sprechen jederzeit gern mit Interessenten über ihre konkreten Verifikations-Anforderungen.“
Weitere Downloads zu diesem Artikel
Firmeninformationen
Weitere Beiträge zum Thema Design-Software, EDA
Alle Artikel des Ressorts
Weitere Beiträge zum Thema Labor, Entwicklung Alle Artikel des Ressorts
© elektronikinformationen.de 2020 - Alle Rechte vorbehalten