Archive for the 'AMS Assertions' Category

Hello!

Do you ever

• wonder what the latest news is for Synopsys Custom and AMS solution? how others are using Synopsys solutions?
• wish you had insight into the latest advances in Synopsys solutions?
• have the urge to send comments to Synopsys team, via your smart phone?

The day you all have been waiting for has finally arrived; our Analog Insights blog is Back! Our mission is to create an interactive place where information can be shared and discussed among our design community, from a pure Analog spice-level circuit to an advanced SOC design.

Because Synopsys Custom and AMS tools portfolio is extremely diverse and comprehensive, our range of topics will vary from analog, RF, to mixed signal from a simulation and design angle. The goal of Analog Insights is to also provide accurate information about the flows or solutions that would benefit our end-users and improve performance and productivity.

For example, you will be able to find:

• List blogs where we would provide tricks and tips to improve simulator performance and convergence (for example “5 tips to spice up…your PLL design :^), I know you are all disappointed..)
• Interview blogs with CAD, design, verification, and modeling engineers to get more insight on their work and their best practices using Synopsys AMS tools
• Technical blogs, where we would go deeper on specific Custom design and AMS subjects
• Industry analysis blogs, where we would capture incoming hot trends in technologies and describe Synopsys solutions
• Webinars, Videos showcasing advanced features and/or flows

We of course welcome your inputs and suggestions on how to improve our blog, as we want it to be innovative, instructive and interactive. I hope you would appreciate and use this blog. See you at our next blog!

If you are reading this, you may have had thoughts on blogging yourself, or perhaps you already are a blogger. One of the most valuable lessons that I have learned from writing a blog is how it can be be used for creating and publicizing my personal “brand”. Personal branding is a way to demonstrate the unique expertise and value that you can provide, to potential employers as well as to colleagues in your profession.

I was first introduced to the topic of personal branding in an article for which I was interviewed by EDN magazine; Life after layoffs: How to move forward after a job loss. Since then I have been asked to share my experience as a blogger with others, most recently at a career networking group hosted by Right Management here in Silicon Valley. My “Top 10 ways to attract subscribers to your blog” may be helpful to you in developing your own personal brand through blogging. You can view the slide show of my presentation here: Developing Your Personal Brand Through Blogging.

-Mike

Hi All,

There was another Accellera discussion this week on the topic of AMS assertions. To be more accurate, the discussion has actually focused more on how to define analog properties in System Verilog. Now this is a great example of the type of “analog meets digital” issue we explore here, but I have to say that I just can’t get this image of square pegs and round holes out of my head on this. You know… you might be able to get them to fit together, but only if you make the peg small enough. And therein lies the issue, at least in regards to sizing a solution to fit a problem… and the problem here is how to improve AMS verification.

If you look at the IEEE 1800^TM Standard for SystemVerilog (which you can download from the link if you have an IEEE Xplore® account), you will see that the spec defines seven types of (logical) properties:

1. sequence
2. negation (NOT a property)
3. disjunction (OR of two properties)
4. conjunction (AND of two properties)
5. if…else (IF A then property B)
6. implication (when A then property B)
7. instantiation (you’ll have to look that one up)

Now it’s no wonder I am an analog guy. Logical combinations (NOT, AND, OR) count as new properties???

In any case, look at my Taxonomy of analog properties and you will see that only categories #4 and #7 are a potential fit with the defined System Verilog digital properties.

1. Connectivity properties
2. Static electrical properties
3. Functional properties
4. Single-event temporal properties
5. Cumulative temporal properties
6. Frequency domain properties
   
7. Mixed-signal interface properties

So, how do we fit the round peg into the square hole? Or should we?

I found this statement from the IEEE 1800 spec to be extremely interesting (pg. 244):

“One of the goals of SystemVerilog assertions is to provide a common semantic meaning for assertions so that they can be used to drive various design and verification tools.”

The SV assertions are specifically designed to work with digital verification tools; digital simulators, formal verification tools, and coverage measurement tools. Should we not then be looking at how to best define analog assertions so that they work with analog verification tools? Looking at the little piece of analog that fits with a popular digital verification language certainly has its merits, but I also think that it leaves too much out when it comes to meeting the actual objective of improving AMS verification.

If we instead look at the problem from the point-of-view of what analog properties are, as the developers of the IEEE-1800 standard did for digital, we can get a much better solution. And, I think that it’s actually not so hard to do.

Each of the analog/electrical properties in my taxonomy can be verified by tools that are in use today. The definition of an analog property can refer to the type of analysis or tool required, just as the digital assertions do. And… just as the Verilog-AMS LRM does for models, with analysis-dependent functions.

In the end, the SV assertions come down to a simple true/false boolean value. If we let the analog tools do what they do best, i.e. analyze analog properties and set pass/fail flags, it would be much easier than trying to fit that round peg into a square hole. In fact, that is very similar to some experimental work done at IIT Kharagpur on verification of time domain mixed-signal properties. I believe that this concept, of using optimized analog property checkers, linked to SV where it fits, is the way to go for comprehensive “analog meets digital” verification.

I hope to hear more of your thoughts on the subject.

-Mike

AMS verification
Accellera
Verilog-AMS
System Verilog assertions
IEEE 1800
Assertion-based verification

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.

-Mike
Accellera
assertion-based verification
AMS assertions
analog properties
System Verilog
Verilog-AMS

Great comments from Jonathan on yesterday’s post, so I will continue the discussion here as a new post so that RSS readers get the latest. Jonathan, thanks again for contributing to the discussion.

I do think that it’s important to start with as broad a scope as possible, to be able to put the assertion-based verification (ABV) idea into proper perspective insofar as the value it may (or may not) bring to AMS verification. What we have so far is an idea that originates in digital verification, which we know is a very different domain based largely on language-based design. The adoption rate for AMS languages has been very slow, when you consider that Verilog-AMS and Verilog-A were first developed over 10 years ago. So… at least to play devil’s advocate… I think it warrants questioning the applicability of the ABV concept in AMS. ABV has not had a broad exposure in the analog design community. Hopefully, this will at least contribute to increased mutual understanding across the analog-digital divide.

>I wouldn’t talk about the electrical properties of circuits.. ONLY of signals

We can narrow down the scope of the properties we wish to assert, but how do you define a “signal”? By the way, in digital ABV assertions are closely related to formal verification of functions, and there is some research underway for AMS formal verification as well.

From M-W.com:
Signal - a detectable physical quantity or impulse (as a voltage, current, or magnetic field strength) by which messages or information can be transmitted.

Maybe it would be more accurate to refer to states, and state variables. I found this example of a digital assertion in one of the papers I read recently:

• Whenever

• r1 is high
• g1 must be high
• through the next two cycles

Now, are “r1″ and “g1″ the state of some flag bits that change very infrequenly, or do they represent rapidly changing pulse streams? I can’t tell. All I know reading this assertion is that the state of “r1″ being high requires that “g1″ stays high for at least two more clock cycles. Another assertion might replace the two clock cycles with an “ALWAYS” qualifier. In power-gated designs, even the supply rails become “signals”. I see increased usage of circuit checking functions that act the same as assertions; to identify disallowed electrical states (e.g. floating nodes, leakage paths, overvoltage conditions, etc.)

> Dynamic (instanteous) – these would be characteristics that could be evaluated by a small signal type of analysis.. – or could be done over time, but otherwise not requiring specific relation ships in time..
– Gain, BW, CMRR,

Small signal, or AC analysis is done with a frequency sweep of linearized models. In my taxonomy I had a category for frequency domain properties, so I think large and small signal behavior would both go there.

> I suspect you are not seeing how many are using Verilog-AMS models in their simulations, as these models DO speed up enough to justify the costs, at least in some simulators, and I know very few companies who are NOT using these models,

I actually do see some increased usage of Verilog-AMS, which has subsumed Verilog-A at least in terms of a language standard. The increased usage is driven by the need for higher verification productivity. However, my perspective is of the entire simulation market for both analog and digital tools. If you look at the total installed base of simulators (SPICE, FastSPICE, A-HDL, D-HDL), A-HDLs represent the smallest segment. This ties directly into the motivation for AMS assertions; when verification signoff is owned by the digital team, they want something that fits into their methodology without incurring any performance degradation. An A-HDL model will always be slower than a digital model. Perhaps faster then SPICE or FastSPICE, or perhaps not… but always slower than digital.

> IOW, you don’t see many AHDL models because your customers know you can’t run the types of tools they do have.

Not sure which tools you are referring too, but we (Synopsys) do have customers making extensive use of Verilog-AMS in our FastSPICE-VCS co-simulation solutions.

>and lets be clear.. the spice syntax is STILL based on archaic punch card technology which is NOT used any more,

Ouch!

Making me feel old there. My very first circuit simulation was a punched card run of ECAP back at the University of Buffalo. Sooooo last century!

>so while I applaud the idea of extending .measure type capabilites, lets also move to a modern syntax – where I will say that verilog has it all over spice..

Yeah, I actually wasn’t suggesting extending .MEASURE at all, just trying to provide the digital folks with some historical perspective. I’m all for getting to a more rubust language standard, but I also personally went through the painful early development of a Verilog-A language that was driven more by arguments over syntax and competitive stall tactics, instead of being driven by what the designers needed. (For more on this, ask me about Antrim’s attempts to introduce the $table function sometime).

-Mike
assertion-based verification
AMS verification
Verilog-AMS
formal verification

Sorry.. that “big word” just slipped out here. Let me explain.

As I discussed here recently (AMS assertions and more…), the Accellera AMS Sub-Committee has begun discussing a proposal to extend SystemVerilog for mixed-signal assertions. This “assertion” thing comes from the world of digital verification, so the first order of business is to develop some meaningful definitions of how the concept would apply (if it does) to analog and mixed-signal. It turns out that there is a lot of very intellectual leading-edge research already underway in this area. Wading through some of the research papers, full of such arcane terms as “predicates”, “dense time”, and “reachability”, tells me that we have a long way to go to translate the work into something that has practical meaning for analog designers. Why, reading through all the abstract algebra makes me crave the smell of molten solder just to get back to what it’s really all about… electronics!

So – taxonomy – that’s just a fancy name for a categorized list. Assertions are used to check “properties”, so we are agreed that we should first develop a list of WHAT kind of properties AMS circuits have, before we try to develop a language for HOW to verify them. N’est pas?

Many a new methodology has failed to reach adoption because it was a solution in search of a problem (and I still have the wounds from trying to launch one or two myself). When you look at how “analog meets digital” here the truth is that “analog property” is a misnomer, or at least not broad enough. What we are really concerned with is verification of electrical properties… because the goal is to build working electrical circuits be they analog or digital. Digital assertions only address logical properties along with their associated (discrete) timing, because that is all that a “signal” is in the digital world. If we try to fit analog signals into this digital solution; i.e. Assertion-Based Verification (ABV), would we solve a real problem?

To further that discussion, here is my contribution to a taxonomy of some electrical properties of circuits that must be verified in order to be successful in silicon. You contributions and input are very much invited.

Taxonomy of Analog & Electrical Circuit Properties

1. Connectivity properties

This category might be thought of as the basic ERC, or electrical rule checks, but given the complexity of modern fabrication processes it can get much more complicated. Examples of simple connectivity properties are proper bulk connections for NMOS/PMOS devices. A more complicated electrical property comes from the prevalence of multiple voltage-domain designs. The circuit must be checked to ensure that no low voltage device is connected to a higher voltage supply than it can handle reliably. In this example, a transistor has a physical property that must be tested against an electrical property of the circuit it is in. Simulation alone can miss this. A tool like Synopsys SpiceCheck traces circuit connectivity and checks rules associated with each device model type in a design.

2. Static electrical properties

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.

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

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

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

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

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

Can we develop an assertion language that would cover a significant percentage of the behavior that needs to be verified in AMS circuits? Measurement languages have been tried before. Can this be more than an academic exercise?

I am looking forward to further discussions that will hopefully lead to better verification solutions when “Analog meets Digital”.

-Mike

AMS verification
System Verilog
Accellera
assertions

I’m Good Enough, I’m Smart Enough, and Doggone It, People Like Me!

-Stuart Smalley

Oh, wait a second… those are affirmations, and we’re here to talk about assertions. Right… sorry for the confusion. (And Apologies to Al Franken).

---

So what is an AMS assertion, you may ask? It’s understandable if there is confusion here, especially if you come from the analog part of this blog audience. If you work in the digital verification world, you are probably already very familiar with the concept. In analog, we are still in the definition stage.

The Verification Methodology Manual for SystemVerilog (or VMM) defines an assertion this way:

“Assertions are observers that monitor signals in the DUT for correct behavior.”

Not part of some self-help program after all! That sounds pretty simple, doesn’t it?

>You mean like .MEASURE statements in SPICE?

Yes, I think the .MEASURE would qualify as an analog equivalent of an assertion. But, as with all things analog/mixed-signal the digital world has it much easier. (See … Because digital design is so easy!).

Personally, I would generalize the VMM definition of “assertion” in this context. Here’s my definition:

An assertion is a means to monitor some property of your design that you must verify in order to meet spec.

Now in the digital world it might make sense to use “property” and “signals” interchangeably. In digital – signals and properties can be simply represented by binary value(s), and the properties to be monitored are event-driven; i.e. they can generally be described in reference to a clock, another binary signal, or some prerequisite sequence of logical states. Everything is described in the time domain.

But in analog… signals are not so straightforward! And many of the properties that must be verified are not even signals per se, nor are they necessarily measured in the time domain.

In digital they use languages, like Verilog, to describe the design. So it’s a natural to add some commands for verification to these languages ; hence SystemVerilog assertions, or the PSL Property Specification Language, two of the IEEE standard verification languages. In analog, we don’t do language-based design… which brings us to the issue of the day. The goal of assertions is to automate design verification. We could definitely use more automation in AMS verification, but how would this assertion concept work? What “language” would we use? And what does an AMS property look like anyway?

All these questions are now being discussed in a new working group of Accellera; the standards-making organization that just recently released version 2.3 of Verilog AMS. I am participating in these discussions, and would like to hear from some of you as we work to define these concepts further. I welcome your thoughts or comments here.

In researching the topic of AMS assertions myself, I came across another event to add to our calendar of AMS Verification-related workshops and conference. SASIMI is the “Workshop on Synthesis And System Integration of Mixed Information technologies”. The next occurrence of SASIMI will be March 9-10 , 2009, in Okinawa, Japan. I was particularly interested to find this paper presented at the 2007 SASIMI workshop: “Analog Simulation Meets Digital Verification – A Formal Assertion Approach for Mixed-Signal Verification“. The authors are from the Universities of Frankfurt, Tuebingen, and the Ilmenau Technical University in Germany. You can click on the link above to can find a copy of the paper online. The topic fits very well with the “analog meets digital” theme that we explore here. It is also a very good example of the work that is going in in several places around the world, to advance the state of the art in AMS verification.

I will be exploring the topic of AMS assertions, along with how we can define AMS properties, more in forthcoming blog posts. There are a surprising (to me at least) number of people working in this area, so I am especially interested in hearing from you.

-Mike

AMS verification
System Verilog PSL VMM
Accellera Verilog-AMS
assertions Stuart Smalley Al Franken daily affirmations