Formal Property Verification of the Digital Section of an Ultra-Low Current Digitizer ASIC

This paper details our experience with Formal Property Verification (FPV) of the digital section of a mixed-signal Application Specific Integrated Circuit (ASIC) for ultra-low current measurements. The ASIC was developed as a prototype front-end for the future version of the CERN RadiatiOn Monitoring Electronics (CROME), which is a safety-critical system. The main functionality could be formally proven even though the design contained several counters. A large number of faults could be discovered and removed. The paper aims to demonstrate FPV with SystemVerilog Assertions on a concrete example to give the reader an idea whether and how FPV can be applied to similar designs.