Extracting hardware assertions including word-level relations over multiple clock cycles

Various mining approaches have been proposed for the automatic generation of temporal assertions from execution traces of hardware designs. These approaches can handle assertions based on LTL formulas or PSL, and many of them can represent word-level relations such as inequalities, additions, and so on. In the existing methods, however, such relations are searched only within a clock cycle. They cannot extract a property such that two values at inputs are added, and its result appears two clock cycles later at an output. We propose a method to extract relations over multiple clock cycles between variables as atomic propositions by analyzing execution traces and to generate assertions including the relations. Our method can also efficiently generate assertions by extracting frequent relations between atomic propositions over multiple clock cycles as propositions, that is, conjunctives of atomic propositions. The experimental results demonstrate the feasibility of the proposed method.