Communication protocol analysis of transaction-level models using Satisfiability Modulo Theories

A critical aspect in SoC design is the correctness of communication between system blocks. In this work, we present a novel approach to formally verify various aspects of communication models, including timing constraints and liveness. Our approach automatically extracts timing relations and constraints from the design and builds a Satisfiability Modulo Theories (SMT) model whose assertions are then formally verified along with properties of interest input by the designer. Our method also addresses the complexity growth with a hierarchical approach. We demonstrate our approach on models communicating over industry standard bus protocol AMBA AHB and CAN bus. Our results show that the generated assertions can be solved within resonable time.