In this paper we present our methods and results on formally verifying the implementation of the Receive Slave SCI-PHY mode of the Transmit Master/Receive Slave (TMRS) design using FormalCheck. TMRS is made of two major modules namely "Internal Register CBI interface" and "SCAN Interface". The SCAN module is responsible for the main functionality of the TMRS block, whereas the CBI module handles the configuration and the test route of it. We produced an abstracted model of the TMRS block. We then provided a number of relevant liveness and safety properties
expressible in FormalCheck, and accomplished their verification on the abstracted model of the TMRS and also on its original model in reasonable CPU time. We found a number of mismatches between the RTL design and the SCI-PHY protocol as well as the TMRS specification. The experience on the verification of the TMRS demonstrates that FormalCheck is powerful enough to be used for verification of real size circuits.

Download postscript file (PS File)

Download PDF file (PDF File)

Send comments and suggestions to: l_baraka@ece.concordia.ca