Multi-clock SVA synthesis without re-writing

This paper presents a compilation procedure for synthesizing multi-clock SVA properties for formal verification. The synthesis framework is built upon an existing compilation algorithm for single-clock SVA properties. While we could use the SVA rewriting rules to transform a multi-clock property into a single-clocked property and then apply existing techniques, instead we propose techniques to selectively model the multi-clock operators to produce a smaller checker logic. Through recursive construction and syntactic transformation, we are able demonstrate the efficiency of the technique and the generated checker logic is provably equivalent to the rewritten version.