2007 Asia and South Pacific Design Automation Conference
Trace Compaction using SAT-based Reachability Analysis
Yokohama
January 23-January 26
ISBN: 1-4244-0629-3
Sean Safarpour, Department of Electrical and Computer Engineering, University of Toronto, Toronto, Canada. sean@eecg
Andreas Veneris, Department of Electrical and Computer Engineering, University of Toronto, Toronto, Canada. veneris@e
Hratch Mangassarian, Department of Electrical and Computer Engineering, University of Toronto, Toronto, Canada. hratch@ee
In today's designs, when functional verification fails, engineers perform debugging using the provided error traces. Reducing the length of error traces can help the debugging task by decreasing the number of variables and clock cycles that must be considered. We propose a novel trace length compaction approach based on SAT-based reachability analysis. We develop procedures and algorithms using pre-image computation to efficiently traverse the state space and reduce the trace lengths. We further introduce a data structure used to store the visited states which is critical to the performance of the proposed approach. Experiments demonstrate the effectiveness of the reachability approach as approximately 75% of the traces are reduced by one or two orders of magnitudes.
Citation:
Sean Safarpour, Andreas Veneris, Hratch Mangassarian, "Trace Compaction using SAT-based Reachability Analysis," asp-dac, pp.932-937, 2007 Asia and South Pacific Design Automation Conference, 2007