Modeling Techniques for Formal Verification of BIST Controllers and Their Integration into SOC Designs

This paper describes the methods and challenges for modeling BIST logic in complex SoCs to enable their verification using formal techniques. The main contributions of this paper are: (a) application of symbolic model checking to BIST logic verification, (b) abstraction and modeling of sequential blocks such as memories, data-loggers, scan chains and LFSRs to enable property based formal verification, (c) automated generation of re-usable hookup logic properties, and (d) experimental results to highlight the benefits of the proposed techniques