Verification of FPGA electronic designs for nuclear reactor trip systems: test- and invariant-based methods

Principles of verification for FPGA electronic design algorithms used in nuclear reactor trip systems are proposed. A classification of the algorithms that is based on complexity criterion is given. Various methods and techniques for testing of the algorithms are described. It is presented an example of verification, based on proposed methods and techniques, for standard algorithm of reactor trip system. Some principal aspects of invariant-oriented verification for FPGA-based safety-critical systems are described.