Formale Verifikation
Lückenlose Prüfung komplexer Chip-Designs im Post-Silicon-Debugging durch Tools der formalen Verifikation
16.02.2010 | Autor: Jamil R. Mazzawi, Pearl Lee, Lawrence Loh*
Wie sich Fehler aufdecken aufdecken lassen
Wenn das Post-Silicon-Debug-Team im getesteten Chip einen Fehler entdeckt, so ist dieser zunächst sehr abstrakt und mit vielen Unbekannten behaftet. Zunächst bemerkt man nur, dass der Chip nicht reagiert, Pakete verliert, falschen Output liefert oder ähnliches. Um der Ursache des Verhaltens auf die Spur zu kommen, muss man wissen, was im Chip passiert.
Viele Chips werden deshalb heute mit Trace-Funktionen ausgestattet. Sie können beim Auftreten bestimmter Ereignisse angehalten werden und interne Logikanalysatoren ermöglichen die Ausgabe bestimmter Signalgruppen an externe Anschlüsse. Die Zustände ausgewählter Signale in einem Zeitraum von n Zyklen vor dem Anhalten lassen sich in einem internen Speicher ablegen, und überdies können die Zustände von Flipflops über Scan-Ketten herausgetaktet werden. Das Post-Silicon-Debug-Team kann sich also darüber informieren, was in den Zyklen unmittelbar vor (und evtl. auch kurz nach) dem Auftreten eines Problems abgelaufen ist.
Gesteuerte Zufallssimulation zum Einkreisen des Fehlers
Die aufgezeichneten Trace-Informationen geben klar Auskunft darüber, dass ein unzulässiges Verhalten aufgetreten ist und was in den letzten n Zyklen vor dem Problem abgelaufen ist. Wie es zu diesem Zustand kam, bleibt jedoch im Dunkeln. Hinzu kommt, dass immer nur eine begrenzte Anzahl Signale beobachtet werden kann und dass die Auswahl der richtigen Signale nicht gerade einfach ist.
Üblicherweise bedient man sich der gesteuerten Zufallssimulation, um den Bug einzukreisen. Wo der Fehler ursprünglich auftritt, ist nicht bekannt. Was man weiß, ist, dass er ein fehlerhaftes Verhalten in Block D zur Folge hat. Der Fehler tritt den Beobachtungen zufolge nach 3- bis 4-stündiger Laufzeit im Labor auf, wenn eine bestimmte Art von Traffic injiziert wird (z.B. nur bei Lese-Transaktionen auf Bus X).Diesem Fehler per Simulation auf die Spur zu kommen, wird meist unmöglich sein. Wenn es im realen Betrieb schon Stunden dauert, bis der Bug auftritt, wieviel mehr Zeit müsste man mit der 1000-mal langsameren Simulation veranschlagen?
Themenverwandte Beiträge
Chip-Design-Debugging: Formale Verifikation mit OneSpin 360 MV erzwingt die 100%-Prüfung
Formale Verifikation: GapFreeVerification-Prozess beschleunigt die formale Verifikation für Module und IPs
Formale Verifikation: GapFreeVerification-Prozess beschleunigt die formale Verifikation für Module und IPs
Formale Assertion-Based-Verification: Neue 360-MV-Produktfamilie von OneSpin macht formale Assertion-Based-Verification breitem Anwenderkreis zugänglich
Formale Assertion-Based-Verification: Neue 360-MV-Produktfamilie von OneSpin macht formale Assertion-Based-Verification breitem Anwenderkreis zugänglich
Kommentare zu diesem Artikel
Lizenzierung urheberrechtlich geschützter Artikel
Nutzen Sie diesen Artikel ID 336406 oder andere Fachinformationen für Ihr Marketing. Wir bieten Ihnen die Nutzungsrechte für Ihre Website, Ihren Newsletter oder Ihre Kundenzeitschrift. Für alle Fragen wenden sie sich bitte an Frau Maurer unter Tel. 0931 / 418-2888 oder unseren Content-Dienstleister www.mycontentfactory.de .
hse-electronic
Flash-Programmierung und Code-Verifikation
Tools für die Flash-Speicher-Programmierung und Code-Verifikation weiter
Langer EMV-Technik GmbH
Bannewitz, Deutschland
pls Programmierbare Logik & Systeme GmbH
Lauta, Deutschland
Debugging von Embedded Linux-Anwendungen auf ARM-Prozessoren
Embedded Linux als Betriebssystem für moderne ARM-Prozessoren? Keine schlechte Idee! Aber da Linux ein Multitasking-Betriebssystem ist, verkompliziert sich das Debuggen von Prozessen. Wirklich?
Embedded Linux als Betriebssystem für moderne ARM-Prozessoren? Keine schlechte Idee! Aber da Linux ein Multitasking-Betriebssystem ist, verkompliziert sich das Debuggen von Prozessen. Wirklich?
Abwärtswandler in der LED-Beleuchtung mit 4 A Ausgangsstrom
Der NCP3125 ist ein Abwärtswandler nach dem Prinzip der synchronen Pulsweitenmodulation. Mit dem Baustein lassen sich Ausgangsspannungen bis 0,8 V einstellen.
Der NCP3125 ist ein Abwärtswandler nach dem Prinzip der synchronen Pulsweitenmodulation. Mit dem Baustein lassen sich Ausgangsspannungen bis 0,8 V einstellen.
Wandler für positive Eingangs- zu negativer Ausgangsspannung
Inverter wandeln positive Gleichspannungen in negative. Die Design-Note „Positive Input to Negative Output Conversion Using a Buck Converter“ stellt zwei Schaltungen mit hohem Wirkungsgrad vor.
Inverter wandeln positive Gleichspannungen in negative. Die Design-Note „Positive Input to Negative Output Conversion Using a Buck Converter“ stellt zwei Schaltungen mit hohem Wirkungsgrad vor.
Auf- und Abwärtswandler mit Batterie für LED-Beleuchtungen
Der LED-Treiber bietet eine Ausgansspannung von 15 bis 22 VDC als Aufwärts- und Abwärtswandler. Der für LED-Beleuchtungen entwickelte Baustein wird mit Batterien betrieben.
Der LED-Treiber bietet eine Ausgansspannung von 15 bis 22 VDC als Aufwärts- und Abwärtswandler. Der für LED-Beleuchtungen entwickelte Baustein wird mit Batterien betrieben.
- Analog & Mixed Signal
- ASIC- & Chip-Design
- Bildverarbeitung
- Daten- & Telekommunikation
- Displays
- Elektromechanik
- Embedded Computing
- Gehäuse & Schränke
- HF & Industrial Wireless
- Labormesstechnik
- Leistungs- & Antriebselektronik
- Leiterplatten
- Messdatenerfassung
- Mikrocontroller & Prozessoren
- Optoelektronik
- Passive
- PLDs & Tools
- Power Management & Stromversorgung
- Relais
- Schalter & Eingabesysteme
- Sensorik
- Speicher
- SPS und IPC
- Verbindungstechnik
- Wärmemanagement
- ASIC- & Chip-Design
- Bildverarbeitung
- Daten- & Telekommunikation
- Displays
- Elektromechanik
- Embedded Computing
- Gehäuse & Schränke
- HF & Industrial Wireless
- Labormesstechnik
- Leistungs- & Antriebselektronik
- Leiterplatten
- Messdatenerfassung
- Mikrocontroller & Prozessoren
- Optoelektronik
- Passive
- PLDs & Tools
- Power Management & Stromversorgung
- Relais
- Schalter & Eingabesysteme
- Sensorik
- Speicher
- SPS und IPC
- Verbindungstechnik
- Wärmemanagement
Copyright © 2012 Vogel Business Media








Home



(nicht registrierter User)