Migrating Assertions From Dense to Discrete Time

Mixed-signal assertions need to be monitored over dense time during analog simulation because analog events are not aligned with clock boundaries in general. On the other hand, simulation of large integrated circuits regularly employs clocked approximations to accelerate the simulation of the analog content in the design. Migrating the analog assertions from the continuous setting to the discrete setting is necessary to monitor compliance in the digital–analog boundary, but such migration must ensure that assertion failures are not missed due to the loss in precision. We propose the formal basis for this migration and a methodology for choosing the granularity of the clock for an assertion in the digital setting.