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.

It is essential to formally ascertain whether the register-transfer level (RTL) validation effort effectively guarantees the correctness with respect to the design's architectural intent. The design's architectural intent can be expressed in formal properties. However, due to the capacity limitations of formal verification, these architectural properties cannot be directly verified on the RTL. As a result, a set of lower level RTL properties are developed and verified against the RTL modules. In a top-down design approach, the architect would ideally like to formally guarantee the coverage of the architectural intent at the time of creating the specifications for the component RTL modules (that is, before they are passed to the designers for implementation). In this paper, the authors present: 1) a method for checking whether the RTL properties are covering the architectural properties, that is, whether verifying the RTL properties guarantees the correctness of the design's architectural intent; 2) a method to identify which architectural properties are still uncovered, that is, not guaranteed by the RTL properties; and 3) a methodology for representing the gap between the specifications in a legible form

It is essential to formally ascertain whether the RTL validation effort effectively guarantees the correctness with respect to the design's architectural intent. The design's architectural intent can be expressed in formal properties. However, due to the capacity limitation of formal verification, these architectural-properties cannot be directly verified on the RTL. As a result, a set of lower level RTL-properties are developed and verified against the RTL. In this paper we present: (1) a method for checking whether the RTL-properties are covering the architectural-properties, that is, whether verifying the RTL-properties guarantee the correctness of the design's architectural intent; and (2) a method to identify the coverage holes in terms of the architectural properties (or their sub-properties) that are not covered.

Existing methods for formal verification coverage compare a given specification with a given implementation, and evaluate the coverage gap in terms of quantitative metrics. We consider a new problem, namely to compare two formal temporal specifications and to find a set of additional temporal properties that close the coverage gap between the two specifications. In this paper we present: (1) the problem definition and motivation, (2) a methodology for computing the coverage gap between specifications, and (3) a methodology for representing the coverage gap as a collection of temporal properties that preserve the syntactic structure of the target specification.

Stuck-at and crosspoint faults in PLA's introduce combinational and sequential redundancies in PLA-based FSM's that affect the testability of these FSM's. We propose a new state assignment algorithm for PLA-based FSM's called EARTH that simultaneously considers area minimization and testability of the resultant PLA's. Our fault model is the single stuck-at and/or single crosspoint fault model. Experimental results show that, on an average, the number of undetectable faults which result due to state assignment by EARTH is about five times less than those generated due to state assignment by NOVA with area overhead 2% more than NOVA.