Efficient BMC for multi-clock systems with clocked specifications

Malay K. Ganai, Aarti Gupta

Research output: Chapter in Book/Report/Conference proceedingConference contribution

12 Scopus citations

Abstract

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.

Original languageEnglish (US)
Title of host publicationProceedings of the ASP-DAC 2007 - Asia and South Pacific Design Automation Conference 2007
Pages310-315
Number of pages6
DOIs
StatePublished - Dec 1 2007
Externally publishedYes
EventASP-DAC 2007 - Asia and South Pacific Design Automation Conference 2007 - Yokohama, Japan
Duration: Jan 23 2007Jan 27 2007

Publication series

NameProceedings of the Asia and South Pacific Design Automation Conference, ASP-DAC

Other

OtherASP-DAC 2007 - Asia and South Pacific Design Automation Conference 2007
CountryJapan
CityYokohama
Period1/23/071/27/07

All Science Journal Classification (ASJC) codes

  • Computer Science Applications
  • Computer Graphics and Computer-Aided Design
  • Electrical and Electronic Engineering

Fingerprint Dive into the research topics of 'Efficient BMC for multi-clock systems with clocked specifications'. Together they form a unique fingerprint.

  • Cite this

    Ganai, M. K., & Gupta, A. (2007). Efficient BMC for multi-clock systems with clocked specifications. In Proceedings of the ASP-DAC 2007 - Asia and South Pacific Design Automation Conference 2007 (pp. 310-315). [4196050] (Proceedings of the Asia and South Pacific Design Automation Conference, ASP-DAC). https://doi.org/10.1109/ASPDAC.2007.358004