Scope < VerilogAMS

VerilogAMS Web>AmsAssertions>RequirementsGatheringGroup>RequirementsWorkingDraft>Scope (2009-02-23, MikeDemler) (raw view)EditAttach
---++ Assumptions 

   1 The resulting assertions will be an extension of SVA and inherit the current semantics of SVA.
   1 New assertion language constructs will be drawn from Verilog-AMS where possible.
   1 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.
   1 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) &gt; 0.5).
   1 Timing checks on waveforms (if V(a) &gt; 0.5 then within 5 us V(b) &gt; 0.5).
   1 Digital to analog interactions (if V(a) crosses 0.5 then a should rise followed by b rising 1 clock cycle later.
   1 Ability to reuse assertions across different abstraction levels (Verilog-AMS, Spice, RTL) with minimal/no changes.
   1 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.
   1 Functional properties, single event temporal properties, cumulative temporal properties, mixed-signal interface properties as defined by [[http://synopsysoc.org/analoginsights/?p=86][Mike's taxonomy]]:
<b><div style="margin-left: 40px;">
   * <span mce_style="font-size: 10pt; font-family: " style="font-size: 10pt;">Functional properties</span>
</div></b><div style="margin-left: 80px;"><span mce_style="font-size: 10pt; font-family: " style="font-size: 10pt;">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&#8217;t work that way. Reading
a netlist doesn&#8217;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 _[[http://hvg.ece.concordia.ca/Publications/Confrences/FDL%2707_02.pdf][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.

</span></div><div style="margin-left: 40px;">
   * <b><span mce_style="font-size: 10pt; font-family: " style="font-size: 10pt;">Signal properties I</span></b> *: single-event temporal properties*
</div><div style="margin-left: 80px;"><span mce_style="font-size: 10pt; font-family: " style="font-size: 10pt;">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 [[http://www.synopsys.com/products/mixedsignal/hspice/hspice.html?BAC-HP&Link=Product_Pulldwn_Home][HSPICE]] pioneered  an automated mechanism for checking this type of circuit property.

</span></div><div style="margin-left: 40px;">
   * <b><span mce_style="font-size: 10pt; font-family: " style="font-size: 10pt;">Signal properties II</span></b><span mce_style="font-size: 10pt; font-family: " style="font-size: 10pt;"> *: cumulative temporal properties* </span><span mce_style="font-size: 10pt; font-family: " style="font-size: 10pt;"></span>
<div style="margin-left: 40px;"><span mce_style="font-size: 10pt; font-family: " style="font-size: 10pt;">This
type of property includes behavior that requires many measurements of
multiple signals, sweeping over time and-or voltage/current in order to
test. Examples are dynamic differential and integral linearity in an
analog-digital converter, jitter, eye-width in a SERDES bit stream, etc.

</span></div>
   * <b><span mce_style="font-size: 10pt; font-family: " style="font-size: 10pt;">Mixed-signal interface properties</span></b><span mce_style="font-size: 10pt; font-family: " style="font-size: 10pt;"></span>
<div style="margin-left: 40px;"><span mce_style="font-size: 10pt; font-family: " style="font-size: 10pt;">The
use of digitally-controlled analog circuits is increasing; because
digital transistors come very cheap on nanometer processes, and because
those processes tend to produce analog behavior with too much
variability to be useful without adjustment. Any property
where an analog value on one side of the mixed-signal interface should
match to a digital code on the other side fits into this category. An
ADC used for measurement purposes, a digitally calibrated current-DAC,
etc. are typical examples.</span></div>
</div><div style="margin-left: 40px;"><div style="margin-left: 40px;">
</div></div><div style="margin-left: 80px;">
</div>

---++ 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.
   1 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.
   1 Static electrical properties as defined by [[http://synopsysoc.org/analoginsights/?p=86][Mike's taxonomy]]:<br />
   * *Static electrical properties*
<div style="margin-left: 40px;"><span mce_style="font-size: 10pt; font-family: " style="font-size: 10pt;">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 &#8220;signal&#8221; to check. Synopsys [[http://www.synopsys.com/products/mixedsignal/hsim/hsimplus_circuit.html][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.

</span></div>

---++ Low interest 
   1 Connectivity properties as defined by Mike's taxonomy. - We are not convinced that the primitives are available to do this easily.
   1 Complex frequency domain properties - a frequency domain property that requires the FFT of a transient simulation or similar function in the analysis.
(from [[http://synopsysoc.org/analoginsights/?p=86][Mike's taxonomy]])<br /><!--[endif]-->
   * <b><span mce_style="font-size: 10pt; font-family: " style="font-size: 10pt;">Signal properties III: frequency domain properties</span></b>
<div style="margin-left: 40px;"><b><span mce_style="font-size: 10pt; font-family: " style="font-size: 10pt;"></span></b><span mce_style="font-size: 10pt; font-family: " style="font-size: 10pt;">This
could perhaps be included in the type II signal properties, but I break
out separately the type of AMS circuit properties that are derived
through frequency domain transformations. Anything to do with harmonic
distortion, signal-to-noise ratio, filter cutoff frequency, etc. falls
into this category.</span></div>

-- Main.ScottLittle - 13 Feb 2009
Topic revision: r4 - 2009-02-23 - 23:38:54 - MikeDemler
VerilogAMS