Adopting an ESL based design and validation methodology, we introduce a top-down approach for efficient debugging of microarchitectural specification and RTL implementation. Our solution is based on the formalism introduced by statistical transactional analysis that we call MAGENTA -- Modeling AGENT for Transactional Analysis. To the best of our knowledge, MAGENTA based root-cause analysis pioneers in the efficient characterization of the micro-architectural design misbehavior via abstraction of validation output by transactions and micro-architectural events.

In this paper w e presen t a lazy model checking approach aimed at improving the efficiency and capacity of symbolic model checking. The lazy approach dynamically computes an abstraction of a circuit model for each pre-image computation based on the partial result leading to the computation. A t the heart of the approach is a lazy algorithm for transition relation building and pre-image computation. A variable minimization heuristic is then proposed to maximize the benefit of the lazy algorithm in iterative fix-point computations. This approach shows greater promise in complexit y reduction than the cone of influence approach.