Symbolic circuit analysis under an arc based timing model
Tools for Automatic Test Pattern Generation (ATPG) typically abstract timing. When a more detailed timing model is needed, either simulation or statistic timing analysis is usually applied. Our symbolic engine based on Satisfiability Modulo Theories can reason over a model using pin-to-pin timing arcs as available after synthesis or after place and route. We study the differences of a simple fixed gate delay versus the arc-based timing model.