Posted by mike demler on October 8, 2008
The Verilog-AMS Technical Subcommittee of Accellera held another in a series of conference call discussions on Tuesday Oct-7, to further explore the topic of AMS Assertions. The meeting began with a review of some work that was published at the workshop on Formal Verification of Analog Circuits, which I wrote about here in June.
In the FAC paper, Analog Property Checkers: A DDR2 Case Study, authors from Verimag and Rambus described the use of analog extensions to the PSL Language for verification of DDR2 memory timing properties. Verimag developed the PSL extensions, which they call Signal Temporal Logic (STL), for the European government-funded project PROSYD: Property-Based System Design.
While setup and hold times may appear to have little to do with analog, in this case the DDR2 spec requires applying a variable correction factor that depends on the slew rate of the data and clock signals. (For more details on the slew derating for DDR2 memories, you can download the JEDEC spec here). This variability turns what might otherwise be a straightforward timing measurement into a more complicated case of analog waveform measurement.
Since the DDR2 setup & hold spec requires measuring two waveforms (data and clock) at multiple points, and under multiple conditions of slew rate, it would fit with category #5 from my Taxonomy of analog properties: Cumulative temporal properties.
Dejan Nickovic of Verimag, one of the authors of the FAC paper, also described an example of using STL to verify erase conditions in a Flash memory example from ST Microelectronics. The erase condition of the Flash memory cells was described in this way:
“… define the erasing condition that holds whenever the wordline signal wl is lower than -6 and p-well pw is above 5.
…whenever an erasing condition holds, the pointwise distance between the source s and p-well pw voltages has to be smaller than 0.1 and the value of pw should not be greater than 0.83 from the value of bitline bl.”
This is a DC property, so it fits with category #2 of my taxonomy: Static electrical properties.
I then briefly described three examples of analog properties that go beyond waveform characteristics:
1. Device-level properties to identify mismatched voltage domains (i.e. a thin-gate device switched to a higher voltage signal). This case could be static (category #2) or single-event temporal (category #4).
2. Situation where power-gating inadvertently creates a floating, high-impedance node. This is the case of “analog-X”, and can be destructive if (through leakage or noise) the node floats to a point that it turns on DC current paths. An author at SNUG Boston recently described how this problem has been addressed by Synopsys CircuitCheck. Again, this phenomenon could be considered to be static or temporal, but with a time constant that is much too long to dynamically simulate.
3. DC leakage paths. With the need to do complex on-chip power management, one of the most common needs for mixed-signal verification involves checking of digitally-controlled power modes. Since there is generally no concept of the power supplies in digital simulations, how would we assert an analog property for a supply in order to check leakage current? This would be a temporal property of a device when it is switched into a leaky state, but could also be checked statically with a tool like Synopsys CircuitCheck.
Following my presentation Ed Cerny, a Synopsys colleague and one of the co-authors of the Verification Methodology for System Verilog, described examples of how features of Verilog-AMS and System Verilog could be combined to implement temporal property checking, as in the initial proposal submitted to the Accellera committee. This is helpful for showing how to address problems that can be fit within the event-driven discrete time domain that is used in the digital world. However, to develop and drive adoption of ABV for AMS, I believe that the broader view of analog behavior will be critical. A proposal has also been made to the committee to broaden the scope of the proposed property specification language for AMS assertions such that it would be independent of any simulation/modeling language (i.e. Verilog/VHDL-AMS). I agree that is the way to go, and we should be exploring that more in future Accellera meetings.