This paper presents a post-silicon debug method for many-core systems that focuses on the transactions among the cores. For each core, we extract a finite state machine that represents its abstracted behavior in terms of communication with other cores. Debugging is performed on execution paths that are generated by traversing multiple state machines of the cores using the transactions that are monitored at run-time. First, we start from the last state of a core-under-debug and provide possible previous states according to the monitored communication behavior of the core. This process is repeated, and a number of possible execution paths are generated. Next, we analyze more detailed behavior of each state over the generated paths using a bounded model checker and also designers’ assertions. This way, we eliminate the infeasible paths as well as finding the constraints on internal variables of the cores that has lead to an error. To show the effectiveness of our method, we have used a distributed deadlock detection and resolution algorithm that is implemented on top of a network-on-chip (NoC) as a case study. We show that using our method, we can successfully backtrack in states of multiple cores in the system as well as finding bugs.