Symbolic debugging of globally optimized behavioral specifications

Symbolic debuggers are system development tools that can accelerate the validation speed of behavioral specifications by allowing a user to interact with an executing code at the source level. In response to a user query, the debugger must be able to retrieve and display the value of a source variable in a manner consistent with what the user expects with respect to the source statement where execution has halted. However, when a behavioral specification has been optimized using transformations, values of variables may either be inaccessible in the run-time state or inconsistent with what the user expects. We address the problem that pertains to the retrieval of source values for the globally optimized behavioral specifications. We describe how transformations affect the retrieval of source values. We present an approach for a symbolic debugger to retrieve and display the value of a variable correctly and efficiently in response to a user inquiry about the variable in the source specification. The implementation of the new debugging approach poses several optimization tasks. We formulate the optimization tasks and develop heuristics to solve them. We demonstrated the effectiveness of the proposed approach on a set of designs.