A mechanism for verifying system behavior includes: (1) A "constraint-based inference engine" and (2) a "constraint-based simulator." The inference engine accepts logical/temporal/data dependencies describing a system implementation and automatically derives new logical/temporal/data dependencies describing the input/output ("black-box") behavior of the system or other aspect of the system's behavior. This capability means that a "behavioral model" can be automatically extracted from a "structural model," thereby supporting "encapsulation" and "information hiding." The simulator is driven by the output of the inference engine and behaves like a cycle-accurate simulator except that it can answer the question: Why does Signal S have Value V at Time T? This capability helps in system debugging since the simulator can immediately provide the user with the cause of an anomalous output value in the form of a behavioral constraint (implication) showing how the output value depends upon specific input values appearing in the simulation.