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.

Mixed-signal components, such as low dropouts (LDOs) and phase locked loops (PLLs), are widely used inside the on-chip power management fabric of low power integrated system-on-chip (SoC) designs. The digital brain of the power management logic that is responsible for regulating the power delivery to different power domains in the chip has to consider the real time latencies of the analog components, which otherwise leads to functional errors in the domains being driven. The latencies may be viewed as contracts between the digital and the analog. This article presents an approach for generating assertions for protecting such mixed-signal latency contracts and using them to rule out timing bugs in the power management logic. Our tool flow enables the verification of the power management fabric, combining a novel mixed-signal assertion checking method in a simulation setting, and a full formal verification method for the digital brain of the power management logic. To the best of our knowledge, this is the first framework where assertions are used for binding analog latency contracts on the digital logic of power management.