Efficient BMC for Multi-Clock Systems with Clocked Specifications

Current industry trends in system design - multiple clocks, clocks with arbitrary frequency ratios, multi-phased clocks, gated clocks, and level-sensitive latches, combined with clocked - pose additional challenges to verification efforts. We propose an integrated solution that improves SAT-based bounded model checking (BMC) by orders of magnitude, for verification of synchronous multi-clock systems with clocked LTL properties. Our main contributions are: a) efficient clock modeling schemes to handle clock related challenges uniformly; b) generation of automatic schedules and clock constraints to avoid unnecessary unrolling and loop-checks in BMC; c) dynamic simplification of BMC problem instances with clock constraints; and d) customized BMC translations - with incremental formulations and learning - to directly handle PSL-style clocked specifications. We demonstrate the effectiveness of our approach on some OpenCores multi-clock system benchmarks.