Automated verification of a System-on-Chip for radiation protection fulfilling Safety Integrity Level 2

The new CERN Radiation MOnitoring Electronics (CROME) system is currently being devel- oped at CERN. It consists of hundreds of units, which measure ionizing radiation produced by CERN's 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 Prop- erty Verification was combined with constrained-random simulation. For the latter the Universal Verification Methodology (UVM) was used. A software framework has been developed that auto- matically creates reproducible results, which are backward-traceable to the functional and safety requirements. Verification completeness was measured with functional, structural and formal cov- erage 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.