Using SystemVerilog assertions to relate non-cycle-accurate to cycle-accurate designs

The problem of the exact temporal relationship between a non-cycle-accurate and a cycle-accurate design is discussed. A non-cycle-accurate design is transformed into a set of equivalent SystemVerilog assertions. An interpretation schema is defined for the translation of these assertions into the time-dimension of the cycle-accurate design. The assertions are then co-simulated or verified. The conditions are identified under which the method is compositional.