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.

• Type: Conference
• Year: 2007
• Where: ASPDAC
• Authors: Malay K. Ganai, Aarti Gupta
• Keywords: ASPDAC 2007, Clock, Clock Constraints, Clocked, Hardware