multi-clock sva synthesis without re-writing
This paper presents a compilation procedure for synthesizing multiclock 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.
sva multi-clock sva assertions