Model Checking Leveraged Error Localization for Complex RTL Designs

Function and security verification has emerged as an important concern in the design of systems-on-chip (SoC) architectures. Bug detection and localization traces the cause of any violation to a compact portion of the design. In this paper, given a design’s correctness and security properties, we present a novel methodology to localize errors in complex RTL models. Also, we discuss how our approach is applied to a large SoC design to debug its security policy violations. We have leveraged the features of a model checker and assertion based verification to achieve this task. To show a variety of debug scenarios, we inject design mutations in the OpenRISC-1200 SoC causing security policy violations in the form of assertion failures, yielding counterexample traces. Through these traces, our algorithm automatically identifies a concise list of signals responsible for causing the security violation.