Assertion-based verification in mixed-signal design

Technology News | October 18, 2011

By eeNews Europe

Introduction

Assertion-based verification (ABV) is a powerful verification approach that has been proven to help digital IC architects, designers, and verification engineers improve design quality and reduce time to market. But ABV has rarely been applied to analog/mixed-signal verification. This article looks at challenges in analog/mixed-signal verification, evaluates how the ABV concept can address some of those challenges, and shows how languages such as Property Specification Language (PSL) and SystemVerilog Assertions (SVA) can be used to write complex analog/mixed-signal assertions.

Assertions, by definition, capture the intended behavior of a design. In verification terminology, ABV can be positioned both as a white-box and a black-box approach in that the user can create properties (or asserted behaviors) that can monitor the design deep within the hierarchy, reaching the internals of the design blocks as well as the interfaces of the design blocks.

Assertions are written both during development of the design and the verification environment. Both designers and verification engineers can consequently be involved in identifying requirements and capturing them as assertions.

So where do mixed-signal assertions fit in?

As design complexity increases, the verification tasks around an analog/mixed-signal (AMS) system become more and more difficult to plan and execute. Some of these fundamental difficulties are:

There is no consistent language or methodology across the complete spectrum of discrete event-driven systems, mixed-signal systems, and continuous time-varying systems to express the verification intent in the form of assertions.
Since no such standard methodology exists, how does information expressed by one group of design or verification engineers in the AMS domain flow to another group, or from one level of design abstraction to another?
In the absence of a standard language and methodology to apply verification to a mixed-signal system in its entirety, how can a verification plan include testing AMS blocks that were tested in isolation in the context of the complete system? This challenge includes verifying aspects such as power sequences, current leakages, and noise figures from the AMS blocks as part of a full-system verification.

The availability of formal property specification languages, with their well-defined set of semantics, has benefited the digital design and verification communities for some time, and in view of the challenges mentioned above, it is natural to attempt to apply the same or similar concepts to the AMS design and verification domains as well. It is with this goal that we show how the standard PSL and SVA languages can be used to extend assertion-based verification to the AMS domains.

But don’t we already have checks and measures in analog?

In the analog verification domain, the idea of developing a specification that drives the need for defining assertions is not a common notion. Nevertheless, analog designers and verification engineers do set custom characterization checks to specify the safe operating conditions for the devices that comprise a circuit. In the Cadence® Virtuoso® Multi-Mode Simulation environment, for example, this is done by adding a special assert device to the circuit and by associating a checklimit analysis to verify if the device-level conditions specified by the user have been satisfied during the course of a simulation that the checklimit analysis corresponds to.

While the application of the assert device along with checklimit analyses is useful to verify the device-level characteristics, there is currently no way to set up and verify more complex circuit conditions that AMS verification tasks encounter. Some of these challenging operations include the ability to predicate assertions on some time-varying circuit characteristics, or the ability to check temporal properties of a circuit at intervals determined by complex clocking conditions.

Moreover, the current use model of using assert and checklimit creates an isolated solution―the methodology only applies to pure analog or mixed-signal applications, and it neither leverages nor makes itself visible to the much broader digital verification methodologies that currently exist.

In contrast, the digital verification system has a well-established use model for assertion-based verification (ABV). This use model is based on standard assertion languages, such as PSL and SVA, and methodologies that have evolved over time to satisfy verification needs in the discrete domain. An optimal mixed-signal verification system will need to leverage the existing principles of ABV and extend them to satisfy the requirements that cannot be met by currently available verification tools.

Along the same line, PSL and SVA will need to expand to accommodate the needs of complex AMS verification challenges. This approach has several long-term benefits:

By extending PSL and SVA to work with mixed-signal languages and semantics, the AMS verification methodology will be able to leverage the existing rich features that are standard in ABV, such as coverage, in a natural way.
There is a growing need for AMS verification to be visible to the overall system verification environment. Toward this end, verification engineers responsible for the overall system need visibility into the verification tasks specified and covered in the AMS subsystem. By using a consistent language and use model from the pure digital to mixed-signal representation, such visibility and information sharing would be natural.

Using PSL with Verilog-AMS

The following sections take a brief tour of the various standard features of PSL and show how these features can support analog and mixed-signal (AMS) expressions. Examples shown in this section use standard PSL code and standard Verilog-AMS, and should be usable in any simulator that supports these languages.

PSL assertions involving analog expressions
For the purpose of this discussion, analog expressions refer to the combination of legal Verilog-AMS operators and operands as defined by the Accellera Verilog-AMS Language Reference Manual. Analog expressions can appear in PSL assertions in Boolean expressions, clocking expressions, and as actual arguments in property and sequence instances when there is a single top-level clock defined either explicitly or via a default clock.

electrical sig;
reg a, b, clk;
// top-level clock specified in the assertion
// psl assert always (V(sig) -> next(b)) @(posedge clk);
// the default clock is inferred as the top-level clock
// psl default clock = (posedge clk);
// psl property P1 = always {a;V(sig1)>0.5} |=> {V(sig2)<1.2;b}; // psl assert P1;

The example above shows how the Boolean expression of a PSL assertion or a property can contain a legal Verilog-AMS expression. For example, referring to the property P1 above, an assertion is being made here that if a is high in the current clock tick and the voltage of node sig1 is greater than 0.5 in the next clock, then wait for one clock cycle and make sure that the voltage of node sig2 is less than 1.2V followed by b being true in the succeeding clock tick.

Analog events for assertion clocking
The Verilog-AMS analog event functions of “cross” and “above” are supported as clocking events in PSL assertions.

electrical sig1, sig2, sig3; reg a, b;
// psl assert always ({V(sig1)>0.5;a} |=> {V(sig2)<1.2;b}) @(cross(V(sig3)));

The example above illustrates that the assertion will be evaluated when the voltage of node sig3 crosses zero in the positive direction within the default time and voltage tolerance, thereby replacing a conventional discrete clock with an object belonging to the continuous domain.

Support for wreal in PSL
The wreal net type represents a real-valued physical connection between structural entities in the Verilog-AMS language. Expressions involving wreal type objects that are explicitly declared can appear in PSL assertions in Boolean expressions, clocking expressions, and as actual arguments in property and sequence instances. The following example shows how expressions involving wreal nets myreal1 and myreal2 can appear inside a PSL assertion:

wreal mywreal1, mywreal2;
reg clk;
// psl assert always ({mywreal1 > 4.4; mywreal2 < 6.6}) @(posedge clk);

Module bound verification units
A verification unit (vUnit) is a side file that is linked to the design file for simulation. A vUnit can be used for analog PSL assertions. This is a very useful feature if the source text of the design block should not or cannot be modified. Thus, the design file remains untouched and the assertion code is provided in the vUnit file, as shown below.

vunit myvunit(test) {
//psl assert (V(sig1) > 1.4) @(cross(V(sig3)));
}

Note that vUnits are mainly used to store the assertion code. However, they are not limited to assertions only. If additional behavioral code is needed for the assertions, like storing some values in variable/registers, it can be added to the vUnit as well. Consider using this feature as it makes the coding of assertions much easier in some cases.
As shown below, verification units can be used to add assertions to Verilog/Verilog-AMS/SystemVerilog, or VHDL instances.

vunit myvunit(test) {
// psl property P1 = ({V(sig1)} -> next (V(sig2)) @(cross(V(sig3)));
//psl assert P1;
}

Support for PSL built-in functions
Analog expressions are allowed within the “prev” PSL built-in sampled value function. It is an error to have analog expressions as arguments to built-in sampled value functions other than prev.

// psl assert always ({V(sigout) > 0.5} |=> {prev(V(sigout)) > 0.4}) @(cross(V(sigout)));

Coverage analysis for PSL assertions
Assertions are an important part of the coverage-driven verification environment. Coverage points indicate whether the stimulus was able to create the conditions necessary to test the design’s behavior. This information is critical to ensuring that the design has been sufficiently tested. This is typically achieved by defining signals and expressions that are being asserted on as coverage points and also by defining the assertions themselves as coverage monitors.

Similar applications of coverage are expected to occur when using assertions in a mixed-signal context. In particular, an assert directive, when comprising mixed-signal expressions in the Boolean layer, will take part in the coverage report and therefore will provide valuable insight into whether the assertions are adequately checking all the analog conditions through which the design is passing. Similarly, creating coverage points for the actual expressions that make up an assertion provide valuable insight into whether the assertion itself needs to be refined to verify the design properly.

Using SystemVerilog assertions in a mixed-signal design
The SystemVerilog language allows a real type to be passed directly through ports. This is a convenient way to bring analog quantities to SystemVerilog, thereby allowing powerful testbench constructs to be developed with these real numbers. The Cadence Incisive® Enterprise Simulator, for example, allows such real valued ports to be connected to nets belonging to the continuous domain by automatically inserting real-to-electrical and electrical-to-real converter elements.

SystemVerilog Assertions (SVA) is a legal subset of the SystemVerilog IEEE P1800-2009 standard. In this standard version, the presence of real data types is not allowed in the Boolean expression layer (although there is a proposal to remove this restriction at the SV-AC technical subcommittee of the IEEE P1800 Working Group). At present, support of real data types in the Boolean expression layer of SVA is limited to vendor-specific implementations. The Incisive Enterprise Simulator allows this and thereby enables users to bring the analog quantity of interest (node voltage, terminal current, etc.) to the SystemVerilog testbench as real numbers and then build powerful SVA constructs using these real numbers. An example follows.

module top;
var real r, xr, wr;
assign xr = 3.14;
ams_electrical_src e_s1(r);
// causes insertion of Electrical2Real
// connection module
ams_electrical_dst e_d1(xr);
// causes insertion of
// Real2Electrical connection module
ams_wreal_src      w_s1(wr);
// Coercion of SystemVerilog real variable
// to wreal
endmodule

module ams_electrical_dst(e);
input e; electrical e;
initial #10 $display(“%M: %f”, V(e));
endmodule

module ams_electrical_src(e);
output e; electrical e;
analog V(e) <+ 5.0;
endmodule

module ams_wreal_src(w);
output w; wreal w;
assign w = 2.5;
endmodule

The example above is a simplified hierarchical design that shows how a wreal net (w inside module ams_wreal_src) can set a real valued variable in a SystemVerilog testbench (top, in this example). It also shows how an object of type var real in SystemVerilog (r and xr) can drive and be driven by objects in the electrical domain (e in ams_electrical_src and e in ams_electrical_dst respectively) with the help of Electrical2Real and Real2Electrical connection modules.

Once a SystemVerilog real variable imports the AMS functionality as shown above, it can appear in any SystemVerilog assertion statement that permits the use of real variables. The simple example below shows how this is done.

simple_SVA_example: assert property (@(posedge(hold)) ((xr-wr) <= 2.5));

Using value fetch to apply assertions to pure analog characteristics
Fetching values of continuous-domain objects into the discrete domain is a common practice that testbench methodologies use to account for mixed-signal effects. Value fetch requires the ability to transcend language boundaries across arbitrary levels of hierarchy through discrete and continuous domain language layers.

Another requirement of value fetch operations is to be able to work from pure digital languages that do not understand continuous-domain syntax or semantics. Such fetch operations usually require a broad spectrum of quantities that may need to be queried such as potential, flow, power, and operating point parameter values. Unfortunately, current mixed-signal languages do not offer such features.

Simulators must therefore provide special features to support such value fetch operations. The Cadence Virtuoso AMS Designer Simulator, for example, has introduced a new system function called $cds_get_analog_value and several helper functions that go with it. The function is used like this:

real x;
always @(…) x = $cds_get_analog_value(“top.sub.end.foo”, “potential”);

The user provides the hierarchical string to the object to be accessed and defines a quantity specifier (in this case potential to the voltage), and the return value is a real number that represents the analog voltage at the moment where the function is triggered.

The syntax of the cds_get_analog_value function is the following:
real $cds_get_analog_value(hierarchical_name [, optional index[, optional quantity qualifier]])where:

The index can be variable, reg, or parameters so long as their value evaluates to an integer constant
The quantity qualifier can be potential, flow, pwr, or param. If none is specified, potential is assumed

The object referred to by hierarchical_name must exist and must be owned by the analog solver. It must be a scalar or a vector, and if the latter, the index must be specified such that the result resolves to a scalar. The hierarchical_name can be a relative or absolute path.

Note: It is possible to check whether the object referred to by hierarchical_name meets these conditions by using the helper functions cds_analog_is_valid, cds_analog_exists, and cds_analog_get_width. These helper functions enable the user to create reusable testbenches where the representation of the model containing the object that the value fetch routine points to can change from digital to analog or vice versa.

The value fetch routine can be called from within Verilog, SystemVerilog, or Verilog-AMS.
The fetch routine needs to reference an analog object. It can reference into any analog language including Verilog-AMS,

VHDL-AMS, Spectre®, SPICE, or Verilog-A (compiled as Verilog-AMS or included by ahdl_include).

Simulation results

The advantage of using standard languages and methodologies that are well established in the digital verification domain in a mixed-signal application becomes apparent when we consider how the results of a mixed-signal simulation employing PSL and/or SVA assertions are displayed graphically.

In contrast to the painful, traditional way of eye-balling waveforms and tracing them back to the failure, designers can use a graphical assertion browser. In the example shown below, the SimVision assertion browser (part of the Cadence Incisive Enterprise Simulator) shows the failed assertions and also the analog and digital signals that constituted the assertions, thereby enabling the user to debug the assertion failure in context.

Summary and future

The objective of this article was to take a broad look at the existing challenges in analog and mixed-signal verification, and then evaluate how an assertion-based verification (ABV) concept can address some of these challenges. We then reviewed a set of examples using the PSL and SystemVerilog Assertion languages that enable users to develop complex assertions on their analog and mixed-signal models. We also showed how such techniques can continue to work in a graphical debugging environment that, to date, has been used almost exclusively by pure digital verification engineers.
Going forward, it appears likely that analog and mixed-signal users will start thinking about developing assertions at the time of block authoring, and use these assertions to communicate the verification intent of their blocks to the outside world, thereby creating a truly unified mixed-signal verification methodology. To support the growing need for using assertions in these areas, it is also expected that the language standardization effort will need to gain momentum such that the analog and mixed-signal aspects of ABV becomes an integral part of the common design and verification languages.

Prabal Bhattacharya has a Bachelor of Engineering degree from Jadavpur University in India in Electronics and Telecommunications. He has been working in various groups in Cadence’s Analog and Mixed-Signal simulation solution for the last 16 years and currently holds the title of R&D Architect. His special area of interest includes mixed-signal simulation and verification, challenges and possibilities in mixed-signal low power, compiler techniques for various analog and mixed-signal languages and software architecture and reuse in simulation products.

Don O’Riordon is a Senior Architect for the Cadence Virtuoso Platform with over 20 years experience in Design & Verification within the EDA industry, having worked at Silvaco on SPICE Modeling, at Transmeta Corporation on CPU verification, and at Cadence Design Systems on a variety of design and verification tools including Spectre circuit simulation, AMS mixed signal simulation and debug, and the Virtuoso schematic capture/analysis environments. Don is the holder of seven patents, and a Masters Degree from the National University of Ireland.