Assumptions

1. The resulting assertions will be an extension of SVA and inherit the current semantics of SVA.
2. New assertion language constructs will be drawn from Verilog-AMS where possible.
3. The assertions will be checked during time domain mixed-mode simulations. Although the focus is clearly on mixed-mode simulations, we would also like to see assertion capabilities added to purely analog simulation use cases. A definition of the subset of the language that can be used in pure analog simulation will be provided.
4. Verification engineers doing AMS verification will be the primary users of the new assertions where AMS verification is defined as verifying systems composed of largely digital components. We believe that there is value in providing assertions for analog designers doing purely analog verification. Providing all of the constructs for both AMS verification and purely analog verification seems impractical, so we will provide a feature set biased to the AMS verification engineer.

Required

1. Comparison of voltage and current values (V(a) > 0.5).
2. Timing checks on waveforms (if V(a) > 0.5 then within 5 us V(b) > 0.5).
3. Digital to analog interactions (if V(a) crosses 0.5 then a should rise followed by b rising 1 clock cycle later.
4. Ability to reuse assertions across different abstraction levels (Verilog-AMS, Spice, RTL) with minimal/no changes.
5. A notion of precision for the assertion constructs using real values (on both time and value) similar to the notion of tolerance used by cross, timer, etc. in Verilog-AMS. This precision should allow for tuning of the precision without introducing discontinuities in the result.
6. Functional properties, single event temporal properties, cumulative temporal properties, mixed-signal interface properties as defined by Mike's taxonomy:

Pretty simple perhaps, but how do you know that a circuit implements the specified function? If we were to automate functional verification, this type of property needs to be included. In digital, the function is defined directly in the design language and formal verification can be applied. SPICE, the primary analog design tool, doesn’t work that way. Reading a netlist doesn’t tell you what the function is, except in very simple cases where you could basically reverse-engineer the schematic. A simple example of an analog functional property is amplifier gain, and any other transfer function property would be included in this category. Some research on this type of functional verification assumes that a functional model is available in an AMS HDL. See Towards Assertion Based Verification of Analog and Mixed Signal Designs Using PSL for example. Complete A-HDL models are still used infrequently however, and the problem of checking the model against the implementation (in SPICE) still would need to be addressed.

This category of analog signal properties is the most like what you would see in a digital assertion. Examples are settling time and other types of time-windowed dynamic signal behavior; overshoot, undershoot, slew rate, etc. The .MEASURE functions in HSPICE pioneered an automated mechanism for checking this type of circuit property.

Nice to have

1. Limited measurement-like capabilities (i.e. similar to Spice measure language constructs). This can be accomplished via user defined functions written in a subset of Verilog-AMS. The subset of Verilog-AMS used to write these measurement functions must have a sound formal definition to ensure formal reasoning about the assertion language and consistent results across simulators.
2. Basic frequency domain properties - given an AC simulation or other simulation where frequency is the independent variable the assertions should provide a way to access to the dependent variable and relate it to the value of the independent variable.
3. Static electrical properties as defined by Mike's taxonomy:
   

• Static electrical properties

With power-managed designs many transistors do not even have a direct connection to a power supply rail. Circuits can be put into standby states where nodes are inadvertently allowed to float, causing potentially destructive leakage paths. The time constants associated with this type of phenomena are too long to be tested in a dynamic simulation, and there is no “signal” to check. Synopsys CircuitCheck performs vectorless voltage propagation to verify static electrical properties. There are other examples as well where this type of verification technique is required to increase verification coverage, and to have observability of behavior that dynamic test benches may miss.

Low interest

1. Connectivity properties as defined by Mike's taxonomy. - We are not convinced that the primitives are available to do this easily.
2. Complex frequency domain properties - a frequency domain property that requires the FFT of a transient simulation or similar function in the analysis.

Mike's taxonomy

• Signal properties III: frequency domain properties

-- ScottLittle - 13 Feb 2009