| The growth in complexity of digital hardware drives an increase in the importance of automated computer-aided design (CAD) tools. Verification consumes most of the design effort, with debugging accounting for half of the verification time. These are therefore important targets for automation. Traditionally, when a failure is detected through an observation value mismatch, an error trace is returned. The error trace can be used with a Boolean Satisfiability (SAT)-based automated debugging tool to aid the engineer in finding the error source. However, when a state is shown to be unreachable, no error trace is available to guide the tool. Debugging these errors is a manual process. This thesis presents two novel automated techniques to perform design debugging in the absence of an error trace. The use of PDR avoids the memory-intensive ILA representation, making it possible to solve larger problem instances. Experiments demonstrate the practicality of the proposed techniques. |
