Using Formal to Exhaustively Determine Unsafe Clock Ratios Between Asynchronous Blocks

Abstract

In this paper we will show how formal property checking can be used to exhaustively sweep the range of allowable clock ratios between any two blocks to determine if their correct operation is maintained. First, we obtain, or create, models of the sending and receiving blocks (in either VHDL or Verilog). After basic functional validation of these models, we then write the property set to reflect the functional requirements of each block. As the clocks between them allow for a range of frequency ratios, we employ the formal analysis principal of nondeterminism to lock-on to a particular supported frequency ratio and prove that the functional requirements are still met.