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, 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.

-- AnandHimyanshu - 09 Feb 2009