Integrated circuit analysis system and method using model checking

A system for analyzing user logic in an integrated circuit under test (ICUT), said ICUT including:

• a user logic (UL) region including a logic circuit operable synchronously with an applied periodic clock, said logic circuit having a plurality of nodes and one or more UL signal lines, each of said UL signal lines extending from an associated one of said nodes, wherein signals on one or more of said UL signal lines are representative of binary values at said associated nodes as a function of time, and
• a debug logic (DL) region including:
• a tracer having one or more tracer (T) input lines, wherein said tracer is responsive to signals on one or more of said T input lines to generate ICUT-based traces, said ICUT-based traces being representative of a succession of states of said user logic circuit over a plurality of cycles of said periodic clock,
• a reconfigurable router responsive to an applied router configuration signal to couple selected ones of said UL signal lines to selected ones of said T input lines,
• a reconfigurable logic responsive to an applied assertion analysis control signal to generate an assertion evaluation signal representative of an evaluation of one or more applied assertions over a succession of clock cycles,
• wherein said system comprises:
• A. a model checker compiler responsive to an applied design description for said ICUT, zero, one or more applied constraints C, an applied initial state I, and one or more applied assertions, to generate basic logic,
• B. a model checker engine responsive to said basic logic to (i) construct a state graph extending from said applied initial state I and representative of plurality of reachable states for said design description with respect to said applied constraints C, and (ii) evaluate said assertions over a subset of said states reachable from said initial state I, and to generate model checker-based traces representative of said evaluation of said assertions over said subset, and
• C. a controller responsive to said basic logic relative to I, C, and said assertions, to generate said router configuration signal for application to said reconfigurable router of said ICUT and transfer said router configuration signal to said reconfigurable router, and being adapted to receive said ICUT-based traces and transfer said received ICUT-based traces to said model checker engine, and
• wherein said controller is responsive to said model checker engine to generate said assertion analysis control signal and apply said assertion analysis control signal to said reconfigurable logic.