Automated verification of a system-on-chip for radiation protection fulfilling safety integrity level 2

Abstract

Ein neues System zur Überwachung von Radioaktivität, genannt CERN Radiation MOnitoring Electronics (CROME), wird derzeit am CERN entwickelt. Es besteht aus hunderten von autonomen Einheiten, welche die radioaktive Strahlung messen, die durch die Teilchenbeschleuniger am CERN produziert wird. Diese Einheiten erkennen gefährliche Bedingungen, wie zum Beispiel Strahlung, die definierte Grenzwerte überschreitet, und unterbrechen den Betrieb der verantwortlichen Maschinen automatisch. Thema dieser Diplomarbeit war die Verifikation eines sicherheitskritischen System-on-Chips (SoC) im Herzen dieser Einheiten. Dem System wurde der Safety Integrity Level 2 (SIL 2) des IEC 61508 Standards für funktionale Sicherheit zugewiesen. Das SoC besitzt einige Eigentschaften, die eine Herausforderung für seine Verifikation darstellen. Es ist hoch konfigurierbar, mit Parametern, die sehr große Wertebereiche haben können. Es wird bis zu 10 Jahre ununterbrochen in Betrieb sein. Gelieferte Messwerte sind abhängig von vorhergehenden Messwerten über die gesamte Betriebsdauer. Das Ziel dieser Diplomarbeit war die Definition und Demonstration einer SIL 2 konformen Verifikationsmethodik für das genannte SoC. Ein automatisiertes Softwareframework zur Verifikation sollte entwickelt werden. Dieses sollte auf Systemebene und für die Reverifikation von zukünftigen Versionen des Systems wiederverwendbar sein. Eine Methodik für unabhängige funktionale black-box Verifikation wurde definiert. Ihr Ablauf beginnt mit der Spezifikation von semi-formalen Verifikationsanforderungen. Natürlichsprachliche Eigenschaften (Properties) wurden vorgestellt und ihre Übersetzung in SystemVerilog Assertions wurde definiert. Formal Property Verification wurde mit constrained-random Simulation kombiniert. Für letztere wurde die Universal Verification Methodology (UVM) angewendet. Ein Software Framework wurde entwickelt, das automatisch Verifikationsergebnisse generiert, die zurückführbar auf die zugrundeliegenden Funktionsund Sicherheitsanforderungen sind. Vollständigkeit der Verifikation wurde Anhand von funktionalen, strukturellen und formarmalen Testabdeckungsmetriken (coverage metrics) gemessen. SystemVerilog wurde verwendet um die Testabdeckung von über viele tausende von Clock-Zyklen verstreuten Werten zu messen. Dazu wurden Covergroups mit Assertions kombiniert. Für gefundene Fehler in der Implementierung wurden spezifische Testabdeckungsmetriken für Regressionstests zu den bereits vorhandenen hinzugefügt. Durch die Anwendung der definierten Methodik konnten einige Fehler in der Implementierung gefunden werden, sowie einige Properties formal bewiesen werden.

The new CERN Radiation MOnitoring Electronics (CROME) system is currently being developed at CERN. It consists of hundreds of units, which measure ionizing radiation produced by CERNs particle accelerators. They autonomously interlock machines if dangerous conditions are detected, for example if defined radiation limits are exceeded. The topic of this thesis was the verification of the safety-critical System-on-Chip (SoC) at the heart of these units. The system has been allocated the Safety Integrity Level 2 (SIL 2) of the IEC 61508 standard for functional verification. The SoC has several characteristics that are challenging for its verification. It is highly configurable with parameters of wide ranges. It will operate continuously for up to 10 years. Measurement outputs are dependent on previous measurements over the complete operating time. The goal of this thesis was the definition and demonstration of a SIL 2 compliant functional verification methodology for the mentioned SoC. An automated verification software framework should be developed that is reusable on system-level and allows the reverification of future versions of the system. A methodology for independent functional black-box verification has been defined. Its workflow starts with the specification of semi-formal verification requirements. Natural language properties were introduced and their translation into SystemVerilog assertions was defined. Formal Property Verification was combined with constrained-random simulation. For the latter the Universal Verification Methodology (UVM) was used. A software framework has been developed that automatically creates reproducible results, which are backward-traceable to the functional and safety requirements. Verification completeness was measured with functional, structural and formal coverage metrics. SystemVerilog covergroups have been used to measure the coverage of values spread over thousands of clock cycles, supported by assertions. Regression coverage has been added to the workflow for discovered implementation faults. Through applying the methodology, several faults in the implementation were found and several properties could be formally proven.