"Easy" Parameterized Verificaton of Cross Clock Domain Protocols

• ABSTRACT:
  
  This paper demonstrates how an off-the-shelf model checker that utilizes a Satisfiability Modulo Theories decision procedure and k-induction can be used for verification applications that have traditionally required special purpose hybrid model checkers and/or theorem provers. We present fully parameterized proofs of two types of protocols designed to cross synchronous boundaries: a simple data synchronization circuit and a serial communication protocol used in UARTs (8N1). The proofs were developed using the SAL model checker and its ICS decision procedures.

• BIBTEX:
  

  @InProceedings{brown_pike_06:2,
    author =    {Geoffrey M. Brown and Lee Pike},
    title =     {"Easy" Parameterized Verificaton of Cross Clock Domain Protocols},
    booktitle = {Seventh International Workshop on Designing Correct Circuits {DCC}: 
                 Participants' Proceedings},
    year =      {2006},
    note =      {Satellite Event of {ETAPS}.  Available at \url{https://leepike.github.io/pub_pages/dcc.html}}}
  

• PAPER DOWNLOAD: pdf 

• SAL FILES DOWNLOAD:
  
  
  • sc.sal (refined synchronizer circuit)
  • uart_constrained.sal (fully parameterized UART with constraints)
  • runproof (proof script)