Working Draft of Requirements for Analog Assertions

The draft has been divided into sections. The primary owners are listed first followed by the secondary owners. Each section has an anchor to it which can be followed to edit the section.

The sections are as follows -

1. General Context
2. Scope of the Assertion Language
3. State of the Art in Digital Assertions
4. State of the Art in Analog Assertions
5. Categories of Analog Designs
6. Expected Use Models
7. User Needs
8. Case Studies and Examples
9. Requirements on Language
10. Requirements on Implementations
11. Interaction between Digital and Analog Engines/Languages
12. Practical Considerations

General Context

• Owner: Kevin Jones

Description of the need for this document and its place in the larger context of the Analog Assertions working group, and in the AMS language/tools effort

Scope of the Assertion Language

• Owner: Scott Little
• Secondary Owner: Mike Demler

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

AMS assertions will be required to check these AMS properties (as defined by as defined by Mike's taxonomy): Functional properties, single event temporal properties, cumulative temporal properties, mixed-signal interface properties.

Definitions:

• Functional properties

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.

• Signal properties I : single-event temporal properties

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.

• Signal properties II : cumulative temporal properties

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.

• Mixed-signal interface properties

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.

Examples of requirements for AMS assertions:

1. Comparison of voltage and current values (V(a) > 0.5). ( single-event temporal property)
2. Timing checks on waveforms (if V(a) > 0.5 then within 5 us V(b) > 0.5). ( cumulative temporal property)
3. Digital to analog interactions (if V(a) crosses 0.5 then a should rise followed by b rising 1 clock cycle later.( mixed-signal interface property)
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.

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

Static electrical properties pertain to electrical conditions of a device that are observable through tests performed at the device terminals, but that are not readilly observable as dynamic waveforms (i.e. within the timescale of a dynamic simulation) .

Example; 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.

(from Mike's taxonomy) <!--[endif]-->

• Signal properties III: frequency domain properties

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.

• Device model properties (added 02/09/09)

Device model properties may be DC electrical parameters (i.e. threshold voltage Vt0) or geometrcial properties (i.e. tox, W/L, etc.). These parameters would typically represent values that could be read-back from the instance of a particular .MODEL in SPICE. Device model properties are distinct from Static electrical properties, in that the latter are dependent on a particular state of a circuit, whereas the former are generally derived from physical properties of a particular fabrication process and the physical layout.

The State of the Art in Digital Assertions

• Owner: Scott Cranston
• Secondary Owner: Ed Cerny

Use Models

There are two basic use models currently used for digital assertions:

• Designers embed the assertions directly in the design. This can be done both at the block level and the subsystem level. These assertions are then passed on to others down the flow to ensure proper use an behavior, document intended use, and to enforce rules of usage
• Verification Engineers (VE) add more complete checks of behavior at a system level. Since VE's are typically not allowed to make changes in the design, these assertions sit off to the side of the design using such capabilities as the PSL vunit or the SystemVerilog bind construct.

Types of Verification

• Dynamic ABV - uses a simulator and a testbench to search for assertion violations
• Formal ABV - formal engine exhaustively explores the state space trying to prove or disprove assertions
• Hybrid ABV - Simulate to a certain spot, then explore the surrounding state space

Languages

• PSL - Property Specification Language (came from IBM Sugar)
  • Relative Strengths: language neutral (Verilog, VHDL, SystemVerilog, SystemC); boolean and temporal layers are not strongly connected, easier to port to a new language
• SystemVerilog Assertions- as name suggests, part of SystemVerilog language
  • Relative Strengths: Allows local variables that carry state
  • Weaknesses: (obviously) very tied to a particular language
• OVL - Open Verification Library - not really a language, a set of models which implement assertion semantics. Typically not used by VE's. Captured by Mentor. IAL (Incisive Assertion Library) is the Cadence-friendly version of this.
  • Relative Strengths: Familiarity (no need to learn a new language). Easier to do things "correctly" as correct usage is enforced.

Standards

• PSL - Accelera
• SystemVerilog - IEEE P1800-2005
• OVL - Accelera OVL 2.3

Tools

• Simulators
  • Cadence NC, Simvision Assertion Browser
  • Mentor Questa
• Formal Verifiers

Description of the current technology in use in the digital world. Languages, use models, tools, standards

The State of the Art for Analog Assertions

• Owner: Himyanshu Anand
• Secondary Owner: Mike Demler

Description of the current approaches for analog. Languages, use models, tools, status

Analog assertions in Industry

Analog assertions are still in the early stages. In the absence of mature tool flows for Analog Mixed Signal (AMS) assertions, engineers have been using workarounds. Some of the methods to apply assertions are presented below. Please feel free to update this section.

• Monitors Only: Checkers are written in Verilog-AMS which verify design intent.

• Monitors with Assertions: Monitors are used to digitize the interesting signals. The digitized signals are then used to verify design properties via assertions like SVA.

( the following is by Mike Demler) Though the concept of assertion-based verification (ABV as digital verification engineers know it) is largely foreign to AMS verification, AMS property checkers have actually been in use in industry for quite some time. The key difference is that the means of applying a property check (i.e. expressing an assertion) is typically not procedural language-based but rather tool-based; i.e. applied through a feature or set of commands provided by a particular AMS design analysis tool (such as SPICE). In some cases, these property checkers can be automated through scripting techniques. These methodologies are not merely workarounds, they are the equivalent tools in the AMS domain which should be understood as the basis for how AMS designs are currently verified. The execution of AMS assertions, through extensions of System Verilog, will still rely on the same core analog engines to derive the signal and circuit behaviors which these tools check today.

Some of the tools and methodologies currently used for verifying AMS properties are:

• The " Designers Guide " methodology , developed by Henry Chang and Ken Kundert, has gained some traction with AMS verification engineers. The methodology applies Verilog-AMS assertions along with scripting techniques to flag violations of functional properties, <!--[endif]-->connectivity properties and single-event temporal properties.
• Proprietary waveform analysis tools: e.g. Cadence Ocean scripting and MDL, Synopsys WaveView analyzer.
• Circuit checkers: Synopsys CircuitCheck
• Real number modeling, SPICE-Verilog co-simulation through PLI 2.0 (see http://synopsysoc.org/analoginsights/?p=39)

Academic Research

Some of the work related to assertions and formal verification of analog mixed signals is provided below.

• Verimag (Oded Maler, Dejan Nickovic, Amir Pnueli) has extended PSL and used property verification on mixed signal designs at ST and Rambus. Signal Temporal Logic (STL) was used for the extension. STL adapted Metric Interval Temporal Logic (MITL) to reason about analog/mixed signal properties. Analog Monitoring Tool (AMT) provides property based monitoring of analog and mixed-signal simulation traces. More information at the http://www-verimag.imag.fr/~nickovic/index.php?id=nickovici&page=amt

• IIT Kharagpur (Pallab Dasgupta and team) has extended SVA and generated monitors, checkers and SVA properties and used them to verify circuits at National Semiconductors. The properties are converted into Verilog-AMS monitors. The monitors digitize the signals which are then used in SVA. "Instrumenting AMS Assertion Verification on Commercial Platforms" by Mukhopadhyay et al. List of other related publications can be found at http://www.facweb.iitkgp.ernet.in/~pallab/formalpub.html.

• University of Utah researchers (Scott Little and Chris Myers) developed a tool to extract formal models of AMS designs by analyzing spice simulations using hybrid Petri Nets. More information at http://www.async.ece.utah.edu/~little/index.html.

• University of Concordia (Sofiene Tahar, Mohamed Zaki), researchers have applied formal methods to verify AMS designs. More information at http://users.encs.concordia.ca/~mzaki/. A survey paper of formal methods for analog circuits is found at http://hvg.ece.concordia.ca/Publications/Confrences/09_NEWCAS%2706.pdf.

Categories of Analog Designs

• Owner: Mike Demler

Description of the kinds of things we are considering as the target for this work. Big D/Little A, Big A/Little D, circuit, RF, Power, AMS, ...

Expected Use Models

• Owner: Scott Little

For the categories described above, describe the ways in which we believe the analog assertions will be used. The kinds of problems and tasks we believe we are attempting to satisfy. Design/Verification. Analog/Mixed mode. Simulation/Formal. Documentation/Checking

Expected Use Models

It is expected that the assertion language will be primarily used in simulation-based mixed-signal verification. The focus of the language should be to provide assertions that can be used by verification engineers to perform functional verification of mixed-signal designs. Currently, the state of the art in formal verification engines for mixed-signal circuits is relatively immature and will not strongly influence language design and features.

The expected use models below can be largely understood in the context of the verification methodology described by Chang and Kundert in their paper entitled "Verification of Complex Analog and RF IC Designs." Briefly, the methodology involves developing behavioral models of the analog blocks. These models are checked against the implementation. The models are also used in block-level as well as system-level verification using self-checking testbenches. Currently the self-checking in these testbenches is done using Verilog-AMS monitors. The expectation is that these monitors can be replaced with assertions.

Definitions -Device-level: a transistors, resistors, etc. fabricated on the IC
-Block-level: a basic unit of the design that is created by a single designer (maybe 2 designers) such as an LNA, ADC, PLL, voltage regulator, I/O pad, op amp, etc.
-System-level: a composition of blocks and potentially "glue logic" that operate together to perform a specific function such as an RF transceiver, power management unit, SerDes, etc.
-Chip-level: the entire IC or SoC
-Performance verification: verifying performance specifications such as SNR, BER, INL, phase noise, jitter, power consumption, etc.
-Functional verification: verifying the function of a given circuit. For example, ensuring that a high value on the enable signal enables the circuit, verifying correct interconnection of blocks, verifying that a given analog value results in the expected digital output in the expected time of an ADC.

Required

The assertions language will focus on providing a solution that largely (if not completely) provides the tools necessary to verify designs in the following scenarios.

User: Behavioral model developer (Analog designer or AMS VE)
Purpose: Model vs. implementation checking
Level: Block
Circuit type: SPICE netlist/Verilog-AMS model
Description: Create a testbench to verify consistency between implementation and model. The model is ideally derived from the specification, but may also contain model design functions that are specified at the system level but not at the block level.

User: AMS VE
Purpose: Model functional verification
Level: Block
Circuit type: Verilog-AMS model
Description: Verify the functional correctness of an AMS block using the Verilog-AMS model. Depending on the size of the block, it may not be possible to verify all desired functionality of a block-level Verilog-AMS model against the implementation. It is still worthwhile to verify the full behavior of the model. This verification IP can be used in an assume/guarantee methodology at higher levels of the hierarchy.

User: VE
Purpose: System-level functional verification
Level: System/Chip
Circuit type: SystemVerilog /Verilog-AMS/SPICE netlist
Description: Verify the functional correctness of the entire system/chip. Verification requirements should focus on issues relating to proper integration of the system/chip. Using an assume/guarantee methodology at this level can be very beneficial and should include running constraints/assertions used at the block level during system/chip-level simulations.

Non-primary Focus Areas Receiving Strong Consideration

These areas do not directly fall within the primary focus area of the assertions language. However, they are closely related and their requirements should be strongly considered during language development. Complications may result in some needed features not being included in the language. In the case of exclusion, the language should be designed with serious thought for near future inclusion of these use cases.

User: Compact model developer
Purpose: Safety/reliability checks
Level: Device
Circuit type: Compact model
Description: Provide a set of assertions that govern safe/reliable use of the device that can be delivered with the device and checked at higher levels of design and verification.

User: Analog designer
Purpose: Functional verification (time domain analysis)
Level: Block
Circuit type: SPICE netlist
Description: This case relates to verifying time domain properties using a time domain simulation. At this level it is common to use waveforms to verify the design. This is useful, but there is still value that can be derived by providing assertions to provide automation and accuracy to block-level analog verification.

User: Analog designer
Purpose: Functional verification (frequency domain analysis)
Level: Block
Circuit type: SPICE netlist
Description: This case relates to verifying frequency domain properties using a frequency domain simulation. Analog designers often run some form of frequency domain simulation. Providing assertion language constructs to automatically verify properties of these waveforms adds useful functionality for analog designers. The properties should require the same constructs as a time domain simulation. There does need to be support for accessing the frequency as the independent variable instead of time.

Non-primary Focus Areas Receiving Weak Consideration

These areas may benefit from the assertions language and should be considered for future treatment. Currently, they are not a priority due to the adequacy of current solutions or to the added complexity they promise to bring to the assertions language. These use cases involve performance verification which tends to be less closely related to traditional digital verification use models than functional verification concerns.

User: Analog designer
Purpose: Functional verification (frequency domain analysis)
Level: Block
Circuit type: SPICE netlist
Description: This case relates to verifying frequency domain properties using a time domain simulation. The Verilog-AMS language does not provide thorough support for these types of analysis. Because the assertion language is based on Verilog-AMS, it is difficult for the assertion language to provide quality support for these types of properties.

User: Analog designer
Purpose: Performance verification
Level: Block
Circuit type: SPICE netlist
Description: This is one of the most time and simulation intensive tasks of the analog designer. The designer must ensure satisfaction of key performance specifications over a wide range of fabrication and operating conditions.

User: VE
Purpose: System-level performance verification
Level: System/Chip
Circuit type: SystemVerilog /Verilog-AMS/SPICE netlist
Description: There are several performance specifications that must be measured at the system/chip-level. Measuring the performance for a subset of operating conditions is often very time consuming for even a single operating condition.

User Needs

• Owner: Kevin Jones
• Secondary Owner: All

A survey of various users representing all categories and uses described above, to ensure that we are taking input from all the constituents of this work.

Case Studies/Examples

• Owner:

Some illustrative examples that both motivate the requirements and will serve as test cases for any proposals

Design based property examples from Freescale:

1. $stable(a) must be true 10 ns before posedge clk and remain stable until 10 ns after posedge clk. (setup/hold time check)
2. When 'a' is true, V(b), is 3.5 V +/- 10%. (switched power supply check)
3. The difference between consecutive measurements of the period of 'b' should be less than 5% of the period of 'b'. (cycle to cycle jitter)
4. The maximum frequency of the periodic signal 'clk' when 'lock' is false must be within 25% of the first frequency measurement of 'clk' after the first posedge of 'lock'. (overshoot)
5. When 'lock' is true the frequency of 'clk' is 100 MHz +/- 5%. (frequency drift)
6. The duty cycle of a periodic signal must be 50% +/- 2%. (duty cycle)
7. The slew rate of V(a) is less than 100 mV/ms. (slew rate)
8. When V(a) == V(b) the value of V(a) should be within 10% of 3.5 V. (crossover point)
9. The average value of V(a) over a 5 ms interval must be greater than 3.5 V.
10. V(a) must not exceed 4.0 V. Pulses shorter than 50 ns are excluded from the check. (threshold crossing w/ short pulse filtering)

Requirements on Language

• Owner: Kenneth Bakalar
• Secondary Owner: John Havlicek

What are the linguistic requirements on the assertion language. Syntax, semantics, relationship to existing digital languages, relationship to existing analog languages

Requirements Accepted by the RGG:

1. The definition will include a formal statement of the syntax and semantics of cross instantiation, including the SystemVerilog bind statement.
2. The assertion language (ASVA) will include as a subset all productions of the SystemVerilog Assertion language (SVA).
3. The ASVA host language may be either IEEE 1800-2009 SystemVerilog, Accellera Verilog-AMS v2.3 or a designated successor language. A future SystemVerilog -AMS formulated with the compatibility of ASVA in mind will also be a host.
4. The semantics of ASVA are a set of rules that determine if a particular behavior satisfies a formula in ASVA. IF the ASVA host language is SystemVerilog then all productions of the SVA subset of ASVA will have the same semantics as the equivalent SVA formula.
5. The ASVA will support assertions that refer explicitly to the relative timing of events (temporal distance). An event is defined in the host language.
6. The ASVA will support Boolean-valued relational operators of the host language on real-valued subexpressions. Real-value subexpressions are interpreted using the semantics of the host language.
7. The ASVA superset will not create syntactic ambiguity in parsing SystemVerilog code when ASVA is embedded in that language—it will "fit in" to this host language without requiring changes to existing productions.
8. We define a simulator as the entity that generates the model behavior and the evaluator as the entity that determines the truth of an ASVA production. The definition of the ASVA will not prevent the evaluator from observing and reporting on the behavior progressively; that is to say as soon (in simulation time) as the truth of the production can be determined.
9. It shall be legal to instantiate a SystemVerilog module or checker within a Verilog-AMS context in a place where a Verilog-AMS module may be instantiated. It shall be legal to bind a SystemVerilog module or checker to a Verilog-AMS target module or modules.
10. Let a SystemVerilog module or checker be instantiated (explicitly or via bind) in a Verilog-AMS context, and consider a port connection of that instantiation. If the port connection would be legal within an instantiation in a SystemVerilog context, then the connection shall be legal unless prohibited by rules of the language extension we are defining. [Non-normative remark: Part of the intention of this requirement is to avoid the need to deconstruct and reconstruct the components of a connection between a SystemVerilog expression and a port of a SystemVerilog container when the connection is perfectly legal in a SystemVerilog context, but the present instantiation is in a Verilog-AMS context. Another intention is to allow expressions in the intersection of Verilog-AMS and SystemVerilog to be connected to ports of richer SystemVerilog types according to the rules already set out by SystemVerilog.]
11. It shall be legal to connect a Verilog-AMS event expression as actual expression to a checker port of type event.
12. It shall be legal to connect a Verilog-AMS expression of an integral type as actual expression to a port with whose type the expression is assignment compatible as specified in SystemVerilog.
13. It shall be legal to connect a Verilog-AMS expression of a real or wreal type as actual expression to a port of a SystemVerilog real type. If the the SystemVerilog real type is other than real itself, then the Verilog-AMS expression shall be treated as type real and conversion rules shall apply as specified in SystemVerilog.
14. It shall be legal to connect a Verilog-AMS expression of type array of real or array of wreal as actual expression to a port whose type is an unpacked array of SystemVerilog real type. If the SystemVerilog real type is other than real itself, then the Verilog-AMS expression shall be treated as type unpacked array of real and conversion rules shall apply as specified in SystemVerilog.
15. Ability to force an analog solve point from within SV. This can be useful to force a periodic set of time points for accurate measurement, obtain accurate measurements based on an event trigger, etc.
16. Ability to access analog events within SV.
17. Access to the double precision time of the last analog time point as well as the value of an analog quantity.
18. Ability to read VAMS quantities from SV. The VAMS value that is read will be equivalent to the value that would be given to a digital request in VAMS. If an exact value is desired then a time point should be forced.
19. Ability to assign a real array to a wreal vector. This is useful to record a series of VAMS time, value pairs as illustrated in the following example:

input a;
electrical a; //Assume a does something interesting
output wtData[0:255];
wreal wtData[0:255];
output wvData[0:255];
wreal wvData[0:255];
//Not allowed today
assign wtData[0:255] = tData[0:255];
assign wvData[0:255] = vData[0:255];
integer i;
integer size;
real tData[0:255];
real vData[0:255];
analog begin
@initial_step begin
i = 0;
size = 256;
end
if(i < size) begin
tData[i] = $abstime;
vData[i] = V(a);
i = i + 1;
end
end

Requirements on Implementations

• Owner:

What are the implementation requirements? Does the language need to be executable to a specific simulation semantics. Speed?

Interaction with Digital Languages and Engines

• Owner: Prabal Bhattacharya

How should these assertions interact with existing digital tools? Simulators, formal engines, existing AMS systems

Practical Considerations

• Owner: Kevin Jones

How pragmatic should we be? Expediency vs. completeness. Short term vs. long term? Balancing ambition wrt available resources. Standards.

-- AnandHimyanshu - 03 Mar 2009