Automatic trace analysis for logic of constraints

Verification of system designs continues to be a major chal-lenge today. Simulation remains the primary tool for mak-ing sure that implementations perform as they should. We present algorithms to automatically generate trace checkers from formulas written in the formal quantitative constraint language, Logic Of Constraints (LOC), to analyze the simu-lation traces for functional and performance constraint vio-lations. For many interesting formulas, the checkers exhibit linear time complexity and constant memory usage. We il-lustrate the usefulness and efficiency of this approach with large designs and traces