Verification of Safety-Critical Electronics

Safety Life Cycle

 

The CROME electronics have been classified as Safety Integrity Level 2 (SIL 2) devices, as defined in IEC 61508, the Standard for Functional Safety of Electrical/Electronic/Programmable Electronic Safety-Related Systems. This standard defines a safety life cycle that follows the V-Model. A customized V-Model for the CROME project can be seen in Figure 1.

model
Figure 1: V-Model for the CROME Measuring and Processing Unit (CMPU), based on IEC 61508.

 

The highlighted steps belong to System-on-Chip verification and validation. They are described in detail below.

Functional Verification of FPGAs

 

Verification is the process of determining whether a system conforms to its specification. Typically 50% of an FPGA development project is spent in verification. With the increasing complexity of FPGA designs, this number has risen in recent years. 

A common metric to measure verification progress is the tracking of functional coverage. Functional coverage measures how many of a design's functions have been verified. These functions are described in the requirements. For safety-critical systems it not only has to be shown that the system fulfils all of its requirements, but it also needs to be shown that the system does not behave in any other way than specified. Therefore, the verification requirements need to contain additional statements that describe the absence of unintended functionalities.

Functional verification of Hardware Description Language (HDL) designs can be divided into simulation-based verification and formal verification. Simulation based verification can only provide evidence that the design behaves as intended for the specific simulation scenarios that have been tested, that is for the specific input stimuli applied at specific design conditions. Simulating all possible input scenarios with currently available computers and tools would take many years. In the contrast formal verification can mathematically prove that a design always behaves as specified for any kind of inputs. Unfortunately formal verification on full system level would often require more human and computing resources than available. The solution is to combine both techniques and benefit from each’s advantages.

 

Constrained-Random Simulation with Functional Coverage and the Universal Verification Methodology (UVM)

 

Simulation-based verification is done by simulating the FPGA in a simulation tool. The tool simulates the behaviour of the HDL code that will be later programmed into the FPGA. A verification engineer can specify input signals that are sent to the Design Under Verification (DUV), i.e. the simulated HDL design. The simulator computes the results which can then be verified by the verification engineer. In early years these activities have been done manually. Today it is possible to write complex automated testbenches that automatically generate constrained random input signals and verify the computed results. The expected results can be generated by a reference model. The reference model for the verification of the CMPU has been written independently from its HDL counterpart. An important concept of safety-critical electronics development has been applied: independence between the design and the verification engineers.

The testbench for the CMPU has been written in SystemVerilog. This language combines features of high-level languages with those of HDLs. It allows object oriented programming, the usage of operating system libraries and can interface with libraries written in other languages, e.g. in C or Python. Additionally to these high-level concepts, it supports parallelized blocks that are automatically executed as separate simulation threads, blocking and non-blocking assignments, 4-state logic and many more hardware concepts.

Constrained random simulation means that input signals to the DUV are generated randomly. The randomization code is guided by constraints that are dynamically applied during a test run. Rather than specifying hundreds of test cases manually, a verification engineer designs test runs with different constraints. This allows the automatic generation of thousands of test cases, far more than one would ever simulate with manually specified inputs. The advantage is furthermore that the range of tested values can be customized. It can be evenly distributed over the whole possible input range or certain ranges can be given higher priorities in order to test corner cases.

The Universal Verification Methodology (UVM) is a verification methodology that builds on best practices in simulation-based electronic design verification. It combines the benefits of all its predecessors. It defines concepts for implementing testbenches in a reusable way. Reusability is facilitated through a simulator- and therefore vendor-independent open-source SystemVerilog library. 

UVM uses many advantages of SystemVerilog, especially its object oriented programming capabilities and preprocessor macros. For functional coverage collection it completely relies on SystemVerilog. A SystemVerilog class becomes a UVM component by being derived from a UVM base class. The factory pattern is used to increase flexibility and reusability by allowing object type overriding after compile time. Type overriding can also happen at runtime, depending on a testbench internal configuration or condition or enforced from the command line. This allows e.g. to reuse the same test case and testbench components for sending several different input sequences to the DUV.

UVM divides a test run into several phases. Testbench components that are registered with the UVM factory can implement code for these phases. At runtime the phases are traversed in a defined order. Each of them has its specific task like configuring the verification environment, applying stimuli or generating reports.

UVM uses Transaction Level Modelling (TLM). Test scenarios can be specified or randomly generated in sequences that can be scheduled in fixed or random orders. The sequences send transactions to the UVM driver, which sends the actual input signals to the DUV. After the simulator has computed the results, a UVM output monitor reads the output signals and combines them to an output transaction. The input and corresponding output transactions are sent to the UVM scoreboard for verifying the results. This scoreboard can interface with a reference model, which can be written in another language, e.g. in C. Input and output transactions can also be passed to a functional coverage collector. 

conception klein

Formal Property Verification

 

Formal verification mathematically proves that a design satisfies its specification for all possible input value sequences. It has been used in hardware verification for many years. In most projects it is only used for critical subparts of a design, mostly for strictly defined control logic and protocols. Computing resources and tool capabilities often don’t suffice to use it on full system. Many different formal verification techniques for hardware and software exist. One of them is Formal Property Verification (FPV).

FPV tools typically implement bounded model checkers to prove properties written in hardware verification languages. Properties might be proven for all possible states, it might be shown by a counterexample that they can be violated or they might be inconclusive. Inconclusive properties can be proven from the initial state up to a certain number of clock cycles, which is then the proof bound. If it can be shown that a design is able to calculate all outputs within this number of clock cycles, the design can be considered as verified. Several commercial tools for formal property verification exist, which are qualified according to the IEC 61508 standard for functional safety. They can directly take HDL code as input. The temporal propositions for these tools can be specified in several languages, e.g. in the Property Specification Language (PSL) or as SystemVerilog Assertions (SVA). These languages extend Linear Temporal Logic (LTL) formulas by sequential extended regular expressions. They can be used to describe repeating scenarios. Like mentioned, formal verification is typically not done on a complete system. Mostly it is accompanied by simulation or emulation. An advantage of using these languages is that they can be directly used in simulation as well, which can serve as a verification of the properties themselves.

Coverage of formal properties can be measured as well. It can be combined with the coverage results of simulation.

due

The content of this article has been taken from Katharina Ceesay-Seitz’s Master’s Thesis

References

[1] European Committee for Electrotechnical Standardization: IEC 61508-2010: Functional Safety of Electrical/Electronic/Programmable Electronic Safety-Related Systems, Standard, Brussels, Belgium, May 2010

[2] Accellera System Initiative: Universal Verification Methodology (UVM), Napa, CA 94558, United States of America, 2014

[3] Katharina Ceesay-Seitz: Automated Verification of a System-on-Chip for Radiation Protection fulfilling Safety Integrity Level 2 (SIL 2), Diploma Thesis, TU Wien, Vienna, Austria, February 2019