Sanjibkumardas.weebly.com
Chapter 1
Introduction
1.1 What is formal verification?
Formally checking whether the implementation satisfies the specification.
[pic]
Figure 1.1 : Formal Verification
1.2 What is property verification?
Property verification is the formal verification when the specification is in the form of properties.
In other words, given a set of properties and an implementation, it is the way to determine whether all runs of the implementation satisfy the given properties.
In practice there are indeed two ways in which property verification is done today. These are :
• Formal Property Verification ( FPV )
• Assertion-based Verification ( ABV )
In both forms, formal properties specify the correctness requirements of the design, and the goal is to check whether a given implementation satisfies the properties.
FPV techniques formally verify whether all possible behaviors of the design satisfy the given properties.
ABV is a simulation-based approach, where the properties are checked over a simulation run - the verification is thereby confined to only those behaviors that are encountered during simulation.
For these reasons, FPV is often referred to as static property verification while ABV is synonymous with dynamic property verification.
.
1.3 The Motivation
Three-fold motivation :
1. Why formal property verification?
Natural languages like English, if used for writing design specifications, may lead to many logical bugs in chip designs. This is due to their inherent ambiguity. Design specifications are interpreted differently by different designers with the result that the designer’s architectural intent is not implemented correctly. In an era, where bugs are costlier than transistors, the industry has realized the significance of formal property verification.
2. Why analog and mixed-signal circuits?
The following data appeared on IBS Corp’s industry reports (2003):
• By 2006, 75% of all chips will include analog circuits.
• While these circuits only make up 2% of the devices and 20% of the area, they are taking 40% of the design effort.
• About 50% of errors requiring redesign are due to errors in the analog portions.
• Therefore, improvements in analog circuit validation methodology are becoming increasingly important.
While formal verification has become part of the design process of digital circuits, its application to analog and mixed-signal design is only in its infancy. This is mainly due to the fact that the mathematical models for such circuits are very different from the discrete, finite-state transition systems that underlie verification of digital systems. Such models are based on continuous dynamical systems governed by differential equations and their verification calls for different techniques, like those developed in the analysis of hybrid systems
3. Why assertion-based verification (ABV)?
Static formal property verification ( FPV ) is typically used to verify small
design blocks, since the formal model checking tools do not scale to designs of large size. Dynamic ABV is the more widely used alternative where properties are monitored during simulation, and any violation is flagged. Since simulation has less capacity problems as compared to FPV, dynamic ABV is used at various levels, ranging from unit level verification to system level verification.
There is a growing need for Dynamic Assertion based Verification (ABV) support within the mixed signal chip design community. Existing assertion languages such as PSL [5] and SystemVerilog Assertions (SVA) [4] cannot express analog and mixed-signal behavior. This is a major problem for chip design companies that design large mixed signal chips, typically having a large digital part and a small but significant analog part. These chips have complex mixed signal behavior-typically analog behavior controlled over time by digital control signals. There are no industry standard formal languages for specifying such properties, and no tools for verifying such temporal mixed signal properties.
1.4 Summary of the project
In this project we have tried to demonstrate an extension of the formal property verification methodologies typically employed for digital designs so that using it verification of analog and mixed signal designs may also be performed with the same ease.
Typically full chip simulation of mixed signal designs is a verification nightmare because of the time required in simulating the analog blocks accurately. On the other hand, use of behavioral models produced by high-level modeling languages like Verilog AMS have enabled mixed signal chip design groups to model and test the full chip functionality before designing the components.
Since the use of behavioral models for analog blocks and Verilog RTL for the digital blocks significantly speeds up the simulation, dynamic mixed signal ABV is likely to play a significant role in this verification task.
The main contributions of this project are :
1. AMS_SVA, a new assertion language based on SystemVerilog assertions. This new language supports electrical signals ( as in Verilog AMS) and predicates over electrical signals.
2. A tool that synthesizes properties specified in AMS_SVA into SVA property checkers and Verilog AMS monitors for those electrical signals in the AMS_SVA assertions. These SVA property checkers when co-simulated with the design (with Verilog AMS monitors instantiated), dynamically monitor the properties.
Chapter 2
Previous attempts at mixed signal verification and related works
For the formal specification of a mixed signal design, we need a mechanism for the expression of the continuous analog component along with a discrete digital part. Hybrid automata was found to be one of the most suitable automation system for the expression of mixed signal systems.
1. Development of hybrid automata
Hybrid Systems exhibit diverse phenomena and to model these phenomena one needs a modeling language that is
• Descriptive, to allow one to capture different types of continuous and discrete dynamics, be capable of modeling different ways in which discrete evolution effects and is affected by continuous evolution, allow non-deterministic models to capture uncertainty, etc.
• Composable, to allow one to build large models of simple components.
• Abstractable, to allow one to refine design problems for composite models down to design problems for individual components and, conversely, compose results about the performance of individual components to study the performance for the overall system.
Modeling languages that possess at least some of these properties have been developed in the hybrid system literature. Hybrid Automata is one such modeling language. The hybrid automata are rich in terms of descriptive power, but are autonomous, i.e. have no inputs and outputs.
An interested reader may refer to “The theory of Hybrid Automata” by T.A. Henzinger [16] for gathering further knowledge on this topic. In this section we present an overview of the approach followed and the limitations of that approach.
In this approach, the state space is divided into a finite number of states where transition is controlled by digital signals and continuous evolution takes place in each state governed by analog variables. This work was done by Henzinger et al.
There exist several problems with this approach:
• The approach is not scalable, that is to say that the hybrid automata grows to unmanageably large size for most practical mixed signal circuits.
• There is a need for LTL(Linear Temporal Logic)-like languages to express properties over mixed signal circuits. The new language needs to provide support for expressing continuous analog variables like voltage and current.
Hence we decided to use dynamic assertion based approach for simulation based verification of mixed signal circuits. We also tested this approach on real-life circuits like that of a battery charger.
2.2 Development of AnaCTL
Conventional temporal logics like CTL(Computational Tree Logic) used for specifying properties of digital systems are not well suited for property verification of analog systems. Hence, Prof. P.P. Chakraborti et al presented a new language, AnaCTL in [11]. In this work they used an FSM for modeling the analog circuits by bounding and discretizing the analog behavior. This underlying FSM is created by repeated SPICE simulations. They showed how to express properties over continuous variables, like nature and shape of waveforms etc.
Problems with this approach:
• The underlying FSM was created by discretizing the transient behavior of analog circuits using Voltage range subdivision and discrete time-steps. Since, we want to capture the continuous nature of the analog circuit, the time-step size is determined by twice the frequency of the sampling block. So, the size of the FSM becomes prohibitively large for most real-life circuits.
• Performing a large number of SPICE simulations makes this process slow.
2.3 The AMS_SVA language and the AMS_SVA_Synth tool
AMS_SVA, a new assertion language developed on the lines of SVA(SystemVerilog Assertions) and Verilog AMS was proposed in his BTech Project by Kapil Modi. The expressiveness of this language was demonstrated on a real-life mixed signal design of a battery charger. It was observed that many interesting correctness requirements of the battery charger design was expressed in this language.
At the heart of our project lies the AMS_SVA language and our project starts where his project ended. We shall look into the details of this language in Chapter 6.
A tool, AMS_SVA_Synth was also built on top of AMS_SVA which synthesized properties specified in AMS_SVA into checkers in Verilog AMS. These checkers, when co-simulated with the design, dynamically monitor the properties.
Limitations:
• There is no single simulation environment that supports both Verilog AMS and SVA. VCS of Synopsis supports SVA, which is completely for digital designs. Cadence has support for Verilog AMS but does not support SVA.
• Synthesis of verilog monitors for the SVA assertions using the tool developed in a previous work [3], makes the process cumbersome.
• The test bench to connect the design and the assertion monitors needed to be written manually.
In our project we have addressed these issues and have come up with an automatic verification tool for mixed signal designs.
We shall look into the details of the AMS_SVA_Synth tool in Chapter 7.
Chapter 3
Comparison of the assertion based verification (ABV) and the formal property verification (FPV) approaches
A main feature of all the property specification languages, which makes them useful in practice for design verification, is the ability to describe sequences of events over time. The property specification languages derive their formalism from few specific types of logics called temporal logics.
1. Temporal Logic
Temporal logics are extensions of propositional logic, where in addition to the familiar Boolean operators (AND, OR, and NOT) we have temporal operators that allow us to specify constraints on the truth of the propositions over time. In other words, temporal logic allows us to specify properties that describe the behavior of a circuit over time.
Let us consider some of the basic temporal operators and their meaning :
X : The next-time operator .
The property Xf is true at a state if f is true at the next cycle. f may be another temporal property or a Boolean property over the state bits. Xf is sometimes read as “next f”, and the operator X is called the next-time operator.
F : The future operator.
The property Ff is true at a state if f is true sometime (at some state) in the future.
G : The global operator.
The property, Gf, is true at a state if f is true always in the future.
U : The until operator.
The property, f U g is true at a state if g is true at some future state, t, and f is true at all states leading up to t.
Let us consider an example to demonstrate the use of these operators.
Example 3.1:
Let us consider the specification of a 2-way priority arbiter having the following interface:
mem-arbiter ( input r1, r2, clk, output g1, g2 )
r1 and r2 are the request lines, g1 and g2 are the corresponding grant lines, and clk is the clock on which the arbiter samples its inputs and performs the arbitration. We assume that the arbitration decision for the inputs at one cycle is reflected by the status of the grant lines in the next cycle. Let us suppose that the specification of the arbiter contains the following requirements:
1. Request line r1 has higher priority than request line r2. Whenever r1 goes high, the grant line g1 must be asserted for the next two cycles.
2. When none of the request lines are high, the arbiter parks the grant on g2 in the next cycle.
3. The grant lines, g1 and g2, are mutually exclusive.
Using temporal logic these three properties may be written as:
1. G[r1 => Xg1 ^ XXg1]
2. G[~g1 => g2] i.e. g2 is the default grant.
3. G[~g1 V ~g2]
But there is one problem with this specification. It never enforces g2 to be high. This has a serious implication. Consider an implementation that never asserts g2, and always asserts g1.None of the properties will be refuted by our implementation and we will be led to believe that our implementation is correct.
Let us add the following property into our specification :
G[~r1 ^ X~r1 => XX~g1]
Adding this property eliminates the problem. It guarantees that g1 is never asserted except in those cases covered by the first property. The second property forces g2 to be high by default.
Having obtained the properties we now look at both the approaches of property verification one by one and make a comparison of the two approaches.
Suppose the designer has come up with the following implementation shown in Fig 3.1.The Verilog code for the module is also given.
[pic]
Fig 3.1.Arbiter Implementation
3.2 The FPV approach
The FPV setup is shown in Fig. 3.2. At the heart of this approach we have a model checking tool.
A model checking algorithm has two main inputs –
• A Model Checker ( formal property verifier )
• A finite state machine representing the implementation.
Role of the algorithm is to search all possible paths of the state machine for a path that refutes one or more properties. If one exists, then the path trace is reported as the counter-example. Otherwise, the model checker asserts that the property holds on the implementation.
[pic]
Fig 3.2. The Formal Property Verification Platform
The objective of model checking is to search for a path in this state machine that refutes one or more properties of the specification.
[pic]
Fig 3.3. Arbiter State Machine
From the figure 3.3 we see that all paths through the state 00 refute the property :
G[ ~g1 => g2]
The model checker will find a refuting path. Since the path also contains the input sequence for which the refutation occurs, it produces a complete counter-example trace with the appropriate inputs that trigger the incorrect behavior of the module.
3.3 The ABV approach
In this approach, we must first write a test bench to drive inputs into our implementation.
The ABV setup is shown in Fig 3.4.
[pic]
Fig 3.4 Assertion-based Verification Platform
We simulate the implementation with the test bench. The assertion checker reads the signals in the interface and monitors the status of the properties. If any of the properties fail during the simulation, the checker reports it immediately. The failure points help the validation engineer to isolate the source of the bug.
[pic]
Fig 3.5 A simple test bench for our arbiter
Note : The implementation of our arbiter has a bug. Consider the case when both requests are low for two consecutive cycles. The specification demands that the grant be parked on g2 (by default), but in our implementation both grants will be low. Though the specification guards against the error, the bug will escape detection because our test bench never creates the relevant cases.
3.4 Comparison of the two approaches
3.4.1 The FPV approach
Advantages :
• The search is exhaustive – all possible runs are considered.
Limitations :
• Capacity concerns.
The main capacity bottleneck in model checking tools is in representing the state machine that needs to be extracted from the RTL. The number of states in the machine typically grows exponentially with the number of concurrent components.
[pic]
Fig 3.6 The State Explosion Problem for FPV
If module Mi has ki states, then the product state machine, M1 || M2 || … || Mn has k1x k2 x … x kn states.
For model checking global properties of the system, we need the product state machine.
3.4.2 The ABV Approach
Advantages
• It is built over the traditional simulation framework and requires nominal additional effort from the validation engineer.
• Does not have any major capacity concerns, since the verification is done over the simulation run.
Limitations
• A test bench is to be written to drive the inputs into the implementation. The complexity of this task grows rapidly with the complexity of the design. This is because the environment of a module is typically constrained by the behavior of the other modules and by the protocol used for their communication.
For example, to verify an endpoint device in a PCI Express architecture, the test bench must model the rest of the architecture consisting of other endpoints, the switches and the root complex.
• Not exhaustive. Only those behaviors that are covered by simulation are examined for property verification. At times, corner cases may get missed out. So, ABV is not effective unless we can force the test bench to create all the relevant scenarios.
Chapter 4
SystemVerilog Assertions
The success of property verification in the industry depends to a large extent on the evolution of language standards for property specification. Currently, there are three major competing languages for property specification, namely, SystemVerilog Assertions (SVA), Property Specification Language (PSL), and Open Verification Library (OVL).
1. Why SVA?
We chose SVA as the language for our project for the following reasons :
1. SVA is part of the System Verilog language – which is a design and verification language. Property specification can be glued with the design and test bench language to create an integrated verification platform.
2. Since SystemVerilog is an extension of the popular Verilog language, the adoption process of SystemVerilog by engineers is extremely easy and straightforward. SystemVerilog enables engineers to adopt a modular approach for integrating new modules into any existing code. As a result, the risks and costs of adopting a new verification language are reduced.
3. For several reasons (not entirely technical) our FormalV research group has been inclined towards System Verilog as a design and verification language and some of the tools developed by this group are based on SystemVerilog.
SystemVerilog is a hardware description language(HDL) developed as an extension of Verilog. It is used to design and document electronic systems and hence can be called as the textual form of electronic circuits and systems. It was developed originally by Accellera to dramatically improve productivity in the design of large gate-count, IP-based, bus-intensive chips. SystemVerilog is targeted primarily at the chip implementation and verification flow, with powerful links to the system-level design flow. This language is simple to learn as it resembles the high level languages like C or Java.
This chapter is not intended to be a comprehensive overview of the SystemVerilog Assertions Language. The complete syntax and semantics is given in the System Verilog LRM [4].The goal of this chapter is to expose the reader to some of the interesting features of the language that we made use of in our project.
2. Assertions
One of the most important features of SystemVerilog is the Assertions, which makes it very powerful and makes the verification and reusability of SystemVerilog code simple. It is the mechanism for verifying the design intent and functional coverage intent. Assertions are used to ensure that the given property holds for the design or not, which can be used to validate the behavior of the design.
Property is either a sequence or implication that is evaluated to true or false.
Let us consider the 2-way priority arbiter discussed in chapter 2 so that the use of SVA assertions becomes clear. Once again the implementation of the arbiter is reproduced in Fig. 4.1. The arbiter has the following interface:
mem-arbiter ( input r1, r2, clk, output g1, g2)
and the following four LTL properties :
P1 : G[ r1 => Xg1 ^ XXg1 ]
P2 : G[ ~g1 => g2]
P3 : G[ ~g1 V ~g2]
P4 : G[ ~r1 ^ X~r1 => XX~g1]
[pic]
Fig. 4.1 : Arbiter implementation
The above 4 properties can be expressed in SVA as :
property P1;
@(posedge clk)
r1 |( ##1 g1 ##1 g1;
endproperty
property P2;
@(posedge clk)
!g1 |( g2;
endproperty
property P3;
@(posedge clk)
!g1 || !g2;
endproperty
property P4;
@(posedge clk)
!r1 ##1 !r1 |( ##1 !g1;
endproperty
Now we describe the meaning of the symbols used in the SVA assertions.
Each temporal property describes a sequence of events. In SVA we capture the sequences of events through sequence expressions.
3. The notion of sequences
• Sequence expressions are the building blocks of SVA.
• A sequence may be defined as a list of SystemVerilog Boolean expressions in a linear order of increasing time. The Boolean expressions must be true at those specific clock ticks for the sequence to be true over time.
• The ##1 operator is equivalent to the X(next) operator of LTL. Therefore, ##1 g1 is true at a state if g1 is true in the next state of the run. The sequence :
##1 g1 ##1 g1
is true at a state if g1 is true in the next two cycles.
• |( is the implication operator.
Since the semantics of LTL is defined over a state machine, the clock is implicit in LTL properties.
This explains the use of the following expression in the first property :
r1 |( ##1 g1 ##1 g1
This expression is evaluated at every posedge of clock, which was our intent while using the G(always) operator in the LTL formula for P1.
Similarly, one can explain the other three properties.
! is the negation operator of Boolean algebra, || is the OR operator used over Boolean expressions.
The property P4 shows an interesting difference between the semantics of SVA and LTL. We have the sequence, !r1 ##1 !r1, in the antecedent of the implication. This sequence matches at time t+1 iff r1 is false at t and t+1.The property specifies that g1 must be false at time t+2 whenever the sequence matches at time t+1.Therefore the matching of the consequent of the implication occurs after the matching of the antecedent succeeds. Thus in SVA the ##1 s are cumulative.
Compare this with the LTL property :
G [~r1 ^ X~r1 => XX~g1]
If r1 is false at time t and t+1, the antecedent of the implication evaluates to true. The consequent XX~g1 is defined with respect to time t, from which we started to match the antecedent, that is, we expect g1 to be false at t+2(specified by the two XX operators).
4.4 Use of Regular expressions in Sequences
A sequence expression describes one or more sequences by using regular expressions. The notion of regular expressions is supported through three repetition operators :
1. Consecutive repetition : The sequence, p[*5], matches when five consecutive states satisfy p.
2. Non-consecutive repetition : This operator is used when we may want to count events in non-consecutive cycles. The sequence, split[=2] ##1 abort matches when the abort event occurs one cycle after the second split event.
3. Goto-repetition : It is slightly different from the non-consecutive repetition. The sequence, split [(2] ##1 abort matches when the abort event occur sometime after the second split event, not necessarily in the next cycle.
Having written our properties in SVA, we must now assert these properties in an interface using an assert statement. This interface is then bound to the module implementing the arbiter design in a test bench using a bind statement..
4.5 SystemVerilog verification methodology
The SystemVerilog verification methodology relies on 3 building blocks, which can be used separately, or all together:
• Stimuli the design using automatically generated random scenarios - constrained-random (CR) test generation.
• Check the behavior of the design (assertions) and the output data (scoreboard) to verify correctness of operation.
• Measure the functional coverage metrics to provide feedback to the generation and analyze progress of verification.
[pic]
Fig. 4.3 The 3 building blocks of SystemVerilog Verification Methodology
Applying the above methods that include iterative process of simulation, debug and coverage measurement is known as Coverage Driven Verification.
The goal of a Coverage Driven Verification methodology is to maximize verification effectiveness and at the same time, minimize redundancy and ineffective verification work.
The SystemVerilog language contains commands and constructs to support CDV including commands for constraint-random generation, assertions and functional coverage measurement.
Measuring coverage is a critical component of the CDV methodology. The SystemVerilog coverage measurement commands (like covergroup and coverpoint) provide feedback regarding the completeness of the verification process and guide the next steps of verification so that effort and resources are applied to improve overall verification.
[pic]
Fig. 4.4 : The SystemVerilog Verification Methodology
4.6 SystemVerilog Direct Programming Interface (SVDPI)
The SVDPI is an interface between SystemVerilog and C that allows inter-language function calls. This means a SystemVerilog task or function can call a C function and conversely, a C language can call a SystemVerilog task or function call. This is done by importing the C function name into the Verilog language using a simple “import” statement.And best of all, one can do all these without an knowledge or overhead of PLI or VPI.
Note: In fact, even importing is not required. Declaring the C function as extern and calling it from the Verilog code works! The C function has to be compiled and linked into the Verilog simulator.
SystemVerilog C
……….. void hello_sv() {
if (p == 1’b1) printf(“HellofromC\n”);
t = hello_sv(); }
………...
Example 4.1 : A Simple DPI example
[pic]
Fig. 4.5 : Today’s simulation environment can take advantage of SystemVerilog’s DPI, which can call SystemC or C/C++ routines directly from Verilog modules or vice versa.(courtesy Synopsis)
Theoretically, DPI is not specifically meant for interfacing C and SystemVerilog only. It leaves the option open to extend the interface to include any foreign language and SystemVerilog.
The SVDPI has lots of more features but only this feature is important from our project point of view. There are also lots of features of SVA such as constructs like intersect, throughout and within for introducing length restrictions in the sequences. Other useful features include the use of local variables for the definition of properties and the use of multiple clocks to write properties. An interested reader may refer to the SystemVerilog Language Reference Manual [4] for a detailed description.
Chapter 5
Verilog AMS
In this chapter we present Verilog AMS, a modeling language that allows users to describe and simulate analog and mixed signal designs using a top-level design methodology as well as the traditional bottom up approaches.
5.1 Features
Verilog AMS supports analog and mixed signal designs at three levels :
• Transistor/gate
• Transistor/gate-rtl/behavioral
• Mixed transistor/gate-rtl/behavioral circuit
Verilog-AMS provides powerful structural and behavioral modeling capabilities for systems in which the effects of, and interactions among, different disciplines like electrical, mechanical and thermal are important.
As such, Verilog-AMS is a language that supports the description of both analog and digital components. It can be thought of as the merger and extension of the two languages, Verilog-HDL and Verilog-A.
Verilog-HDL mainly deals with the digital signals which are discrete event signals with discrete values. Further information on Verilog-HDL can be obtained from [8].
Verilog-A is designed to model analog signals, signals that vary continuously with time. This can occur in two ways, either this is piecewise constant versus time or continuous versus time. A detailed discussion of Verilog-A can be found in chapter 3 of [7].
Fig 5.1 : Verilog AMS : Merger and extension of Verilog-HDL and Verilog-A
5.2 Mixed-Signal Simulators
Mixed-signal simulators, by their very nature combine two different methods of simulation :
• Event-driven as found in logic simulators, and
• Continuous –time simulation as found in circuit simulators.
As such, they are said to have two kernels; a discrete-event kernel and a continuous-time kernel. These two kernels are an essential feature of any mixed-signal simulator. Indeed it is what separates mixed-signal simulation from other types of simulation.
Verilog-AMS makes it substantially more straightforward to write behavioral models for mixed-signal blocks, and brings strong event-driven capabilities to analog simulation, allowing analog event-driven models to be written that perform with the speed and capacity inherited from the digital engines.
5.3 Applications of Verilog-AMS
There are five main reasons why engineers use Verilog-AMS :
1. to model components,
2. to create test benches,
3. to accelerate simulation,
4. to verify mixed-signal systems, and
5. to support the top-down design process.
Verilog-AMS has certain new data types like real, integer, logic, electrical and ground to express the mixed-signal designs. Moreover, there is no need for explicitly providing connecting interface modules between analog and mixed signal components.
Verilog-AMS has built-in operators for differentiation and integration since analog circuit behavior is often expressed as a differential equation. In the next sections of this chapter, we discuss those features of Verilog-AMS which are important from our project point of view. An interested reader may refer to the Verilog AMS Language Reference Manual [10] or [7] for a detailed description.
5.4 Voltage and Current contributions
Verilog-AMS uses the branch contribution operator calltf = hello;
10 task_data_p->compiletf = 0;
11
12 vpi_register_systf(task_data_p);
13 }
14
15 // Register the new system task here
16 void (*vlog_startup_routines[ ] ) () = {
17 registerHelloSystfs,
18 0 // last entry must be 0
19 };
Invoking the system task
The new system task can be called in initial blocks or in always blocks as shown below:
1 module hello_pli ();
2
3 initial begin
4 $hello;
5 #10 $finish;
6 end
7
8 endmodule
This example was pretty simple and easy to understand.
In our project we made use of the VPI routines which would help us access the values of various signals in the design under test(DUT) at each simulation step. Some of these routines are vpi_iterate, vpi_scan, vpi_chk_error, vpi_handle, vpi_get, vpi_printf etc.The details of these routines can be obtained from the Verilog AMS LRM [10].
Chapter 6
The AMS_SVA Language
In this chapter, we introduce a new language, AMS_SVA which can be called as an extension to the SystemVerilog Assertions language (SVA). To understand the full power of the AMS_SVA language, one must have a basic knowledge of the SVA language. For this reason SVA has already been discussed in Chapter 4.
6.1 The need for a new language
When the mixed signal designer wants to verify his design intent, he needs to specify the properties to be checked over the design. In Chapter 1, we have stressed on the fact that using natural languages like English to specify properties may lead to ambiguous specification. So, there is a need of an assertion language which could specify the mixed signal properties. SVA, as such, is capable of specifying properties only for digital designs.
In Chapter 4, we have highlighted the reasons for choosing SVA as the model for our new language. Before we continue with the formal discussion on the syntax and semantics of AMS_SVA we shall consider a design of a battery charger, which is a fair representative of the class of mixed signal designs.
6.2 The Battery Charger
Large mixed signal chips, designed by the chip design companies, typically have a large digital part and a small but significant analog part. These chips have complex mixed signal behavior, typically analog behavior controlled over time by digital control signals.
The reason for choosing the battery charger as the design for our project is that it is an excellent representative of the typical mixed signal chips. Let us analyze the block diagram of the battery charger shown in Fig. 6.1 to find out why it is so.
[pic]
Fig. 6.1 : Architectural Block Diagram of a Battery Charger
The battery charger consists of two important components :
• Digital Controller : It determines the mode of operation of the analog circuit. It is a state machine whose state transitions are triggered by events from the analog part on continuous variables like voltage (V_battery) and current (I_charger). The digital controller has an output port, fsm_state which indicates its current state. Depending on the fsm_state, the charging voltage (V_battery) and the charging current (I_charger) are set. Fig. 6.3 shows the finite state machine (FSM) for the digital controller.
• Analog circuits : These are responsible for producing analog signals and events that trigger the state transitions of the digital controller. The digital control signals from the digital controller, in turn, determine the mode of operation of these circuits.
Let us now look into the charging profile of a battery charger shown in Fig. 6.2.
Each distinct region in the profile corresponds to a distinct state of the battery charger.
[pic]
Fig. 6.2 : Charging profile for the battery charger
There are generally two types of properties that can be written on these mixed signal designs :
1. State Property : These are the analog properties that characterize the analog behavior of the design at a given state of the controller.
For example, a state property could be :
When the controller is in the pre-charge mode, the charging current should be constant at I_low with tolerance r% and the battery voltage V_battery should be less than V_threshold.
2. Transition property : These properties specify the enabling condition of state transition of the controller.
For example, a transition property could be :
When the controller is in the pre-charge mode and the battery voltage exceeds V_threshold, the controller makes a transition to the constant current mode.
For the various modes of the controller refer to Fig. 6.3.
Having studied SVA in Chapter 4, it must be clear that these properties involving analog signals cannot be expressed using it.
[pic]
Fig 6.3 : FSM for the Digital Controller of the Battery Charger
We list all the properties that should ideally hold for this battery charger and also the corresponding properties in AMS_SVA language in Appendix.
Let us quickly have an overview of the AMS_SVA language.
6.3 The AMS_SVA Assertion Language
We have already seen in chapter 4 that the sequence expressions form the building blocks of SVA. We have introduced two new concepts into the grammar of SVA so that it becomes powerful enough to represent mixed signal properties :
1. A new non-terminal ANAPROP which represents Boolean expressions over electrical variables and their real values.
For example, in order to express that the battery voltage V(B) must be greater than 0.2V the expression under ANAPROP would be (V(B)>0.2). This ANAPROP term evaluates to true when V(B) is greater than 0.2V and false otherwise.
2. A new operator called first_occurrence. This operator can only be applied on an ANAPROP. Typically, first_occurrence(V(B)>0.2V) is true when V(B) crosses 0.2V for the first time in a simulation.
This operator is useful for expressing properties like rise time, settling time etc.
Example 6.1 : Consider the following example :
Suppose we have a LCR circuit as shown in Fig. 6.4 for which the following rise-time property is defined :
The voltage at a port ‘a’ should reach 90% of the maximum value Vmax within n clock cycles from the time it crossed 10% of Vmax.
So here, we need to know when V(a) crossed 0.1Vmax for the first time and hence the first_occurrence operator comes in handy.
The intent can be written as the following AMS_SVA assertion.
first_occurrence(V(a) > 0.1 *Vmax) |( ## [0:n] (V(a) > 0.9 * Vmax)
[pic]
Fig. 6.4 : A simple LCR circuit
6.4 Extension to the grammar of SVA
The complete grammar of AMS_SVA can be found at the Appendix. A large part of it is the same as that of SVA. In this section we highlight only the extended features of the grammar.
• EXP ( (EXP || EXP) | (EXP && EXP) | !EXP | p | ANAPROP | first_occurrence(ANAPROP), where p belongs to AP | epsilon.
Here ANAPROP and first_occurrence have been introduced.
• ANAPROP ( TERM COMPOP TERM
• TERM ( TERM ARITHOP TERM | (TERM) | ddt (TERM) | idt (TERM) | integer | real | ANAVAL
• ANAVAL ( V(p1,p2) | V(p1) | I(p1,p2) | where p1,p2 belong to AP_A.
• ARITHOP ( + | - | * | /
• COMPOP ( < | = | =
5. Semantics of the new constructs
• ANAPROP represents a Boolean variable which holds true when TERM COMPOP TERM evaluates to true.
• first_occurrence (ANAPROP) represents a Boolean variable which evaluates to true at only one time instant when ANAPROP becomes true for the first tme during the simulation run.
• V(p1,p2) : voltage between electrical ports p1 and p2
• V(p1) : voltage between electrical port p1 and ground.
• I(p1,p2) : current between electrical ports p1 and p2.
• I(p1) : current between electrical port p1 and ground.
• ddt (TERM) : differential term
• idt (TERM) : integral term
There is a subtle difference between the first_match operator of SVA and the first_occurrence operator of AMS_SVA.
first_match(s) gives a match at the first time a match is found for every evaluation of sequence s, whereas first_occurrence(s) gives a match only at the first time during the simulation run when s holds true.
Chapter 7
The AMS_SVA_Synth tool
In this chapter, we present the tool developed by Kapil Modi as a part of his BTech Project. This tool synthesizes mixed signal monitors with the specifications expressed in AMS_SVA language.
7.1 Reasons for choosing Verilog-AMS
In chapter 5 we have looked into the salient features of Verilog AMS which makes it extremely useful for mixed signal designs. Here we further highlight the reasons for synthesizing the monitors in Verilog AMS:
1. Generation of monitors in an Accellera accepted standard language like Verilog_AMS makes this tool vendor-independent and this tool can be used in any simulation platform that supports Verilog-AMS.
2. Verilog –AMS provides with inbuilt operators like differentiation and integration. It also provides a simple way to access electrical variables like voltage and current.
3. This tool uses a part of the SVA_Synth tool developed in [3] which synthesized verilog monitors for SVA assertions. Since, Verilog is a subset of Verilog-AMS, so this tool is compatible with Verilog-AMS.
7.2 AMS_SVA_Synth : The Tool Architecture
[pic]
Fig. 7.1 : AMS_SVA_Synth : Tool flow
Fig. 7.1 shows the tool flow of the AMS_SVA_Synth.
The working of the tool can be summarized as below :
Input : AMS_SVA assertions
Intermediate output : Monitors for the corresponding assertions in Verilog and Verilog AMS.
Simulation : The test bench together with the assertion monitors drive the simulation.
Final Output : Dynamic ABV report, containing information about the match and fail of the assertions.
7.3 Components of AMS_SVA_Synth :
• GenSVA_ANALOG_assertions :
This block identifies the analog blocks in the AMS_SVA assertions and replaces these blocks by Boolean variables. Now the properties are in pure SVA as they contain no analog part.
• GenSVAmonitors :
The details of this tool are given in [3].This tool generates Verilog monitors from the pure SVA assertions obtained from the previous part.
• GenANALOGmonitors :
This block generates the Verilog AMS monitors for the analog events identified by the first component. These monitors check the analog variables during the simulation run and when the analog event holds, the corresponding Boolean signal(as generated by GenSVA_ANALOG_assertions) is asserted.
• Gen_Monitor_for_property :
The Verilog monitors generated by the second component and the Verilog AMS monitors generated by the third component are integrated in this step to generate one monitor for each property.
Let us work out a simple example so that the working of the tool becomes clear :
Example 7.1 : Let us consider a mixed signal design having digital inputs ‘a’ and ‘b’ and electrical ports X and Y. Let P be an AMS_SVA property of this design.
P : (((V(X) > 0.2) && a) ##[5:8]b) or ((V(X) < 0.9)[*3:8]) |( I(X,Y) ==0.
Steps :
1. First the analog blocks are identified.
A = { (V(X)>0.2), (V(X)>0.9),(I(X,Y) == 0) }
2. Each ANAPROP in A is replaced by a Boolean variable in P, say v1,v2……
So, P now looks like :
P’ : ((v1 && a ##[5:8]b) or v2[*3:8]) |( v3
These 2 steps are performed by the first component, namely GenSVA_ANALOG_assertions.
3. The component GenANALOGmonitors generates Verilog AMS monitors for the ANAPROPs in A. These monitors are very simple to generate :
For example , the Verilog-AMS monitor for an analog event
e : V(a) > 0.9 would look like
module AMS_SVAe (a,v1);
input a;
output v1;
electrical a;
logic v1;
always @(above(V(a)-0.9)) v1=1;
always @(above(0.9-V(A)) v1=0;
endmodule
4. The component GenSVAmonitors generates SVA monitors for the SVA property P’. This is done using the tool developed in [3] as shown in Fig. 7.2. This machine has the a,b,v1,v2 and v3 as input and asserts a match when P’ matches.
5. The interconnections between a,b,v1,v2,v3 are done and we finally have one monitor for the property.
[pic]
Fig. 7.2 : Monitor synthesis for example 7.1
Integration of the monitors with the DUT
The monitors have to be now instantiated in the test bench of the DUT. This instantiation has to be done manually.
Chapter 8
The AMS_SVA_Verify
1. The need for another tool
The AMS_SVA_Synth tool discussed in chapter 7 seems to be complete, but here are certain limitations with this tool.
1. There is no single environment that supports both Verilog AMS and SVA.
For example, AMSDesigner from Cadence supports Verilog-AMS but not SVA.
VCS of Synopsis, on the other hand, supports only SVA and no Verilog-AMS.
This poses a serious hindrance to the running of the tool automatically. As a result, it resorts to using the tool developed in [3] for synthesizing Verilog monitors for SVA assertions and then using the resulting monitors in the Verilog-AMS environment. This step makes this tool a little cumbersome.
2. Moreover, the tool is not automatic. Even after the generation of monitors, they have to be instantiated manually into the test bench.
3. Treats all types of monitors equally, which might lead to problem as we shall discuss later in this chapter.
8.2 The Plan
The plan is, if somehow we can communicate between the two environments, NC-SIM of Cadence and VCS of Synopsis, then we can get rid of Verilog monitor synthesis for SVA properties, the main bottleneck in the previous tool. We also have to achieve complete synchronization between the two environments and above all, everything must be push-button!!!
8.3 Solution
At the heart of our new tool lies the creation of a synchronized communication channel between the two environments. What is interesting is that no sophisticated mechanism is required to achieve such a communication. A simple named pipe would solve the purpose; named because the two processes running are completely unrelated.
Let us now look into the compete tool flow shown in Fig. 8.1 and understand how things work :
Inputs : DUT ( all the design modules),
Test bench to feed the DUT, and
AMS_SVA property files
Outputs : Dynamic ABV report
8.4 Tool Flow
Steps :
1. The GenSVA_ANALOG_assertions takes as input the AMS_SVA assertions file.It parses the file to identify the analog blocks.Replaces these analog blocks by Boolean variables.The output from this component is a pure SVA property file.
2. The GenAnalog_monitors synthesizes Verilog AMS monitors for the identified analog blocks. The outputs of these monitors are the Boolean variables that were used to replace the analog blocks.
3. The generated analog monitors are then automatically instantiated in the test bench.
4. The DUT, together with the Verilog AMS monitors and the test bench is simulated in the Cadence environment.
5. The VPI feature of Verilog AMS helps to probe into the design modules and extract the values of those signal on which properties are written. These values are extracted at every clock cycle and written into the pipe.
[pic]Fig. 8.1 : The Complete tool flow
6. At the same time, a dummy module is created in the Synopsis environment. The purpose of this module is to just to read the signal values from the pipe by calling a C function using the SVDPI. For the creation of dummy module, the tool refers to the SVA property files for the relevant signal names and also the test bench so that the dummy is in synchronization with the test bench.
7. The dummy module reads the signal values at every clock cycle using the SVDPI.
8. An interface binds the SVA property checker files with the dummy verilog module.
9. A dynamic ABV report is generated by the interface, which gives information regarding which properties matched and failed.
In the previous chapter we have already seen how the analog blocks are replaced by Boolean variables in the AMS_SVA files and how the synthesis of Verilog AMS monitors is done.
8.5 Is there any difference between the different kinds of monitors that are generated?
Yes. All monitors should not be treated in the same way.
If we want to place more than one voltage monitors between two electrical ports, these monitors should be placed in parallel, but if we want to place more than one current monitors between two electrical ports, the monitors must be placed in series.
This is a very important concept and should be taken care of while instantiating the monitors in the test bench.
Example 8.1 :
Consider 2 analog propositions V(p1,p2) > 0.9 and V(p1, p2) 0.9
In this case the two monitors would be
I_mon1(p1,p2,v1);
I_mon2(p1,p2,v2);
Instantiating them in the same way would lead to placing of these monitors in parallel.
Our tool takes care of such situations by creating a false node say n and making the instantiation as :
I_mon1(p1,n,v1) and I_mon2(n,p2,v2).
Chapter 9
Results, Conclusions and future work
We used the tool developed in our project on an industry standard mixed signal design of a battery charger. The battery charger design was available to us in Verilog-AMS.
9.1 Results
Our tool is capable of verifying all the seven properties of the battery charger that we have listed in Appendix B. Interestingly, we were able to find few bugs in the design. Also we introduced a few bugs deliberately and checked if our monitors could successfully discover those bugs.
Table 9.1, shows the simulation time with and without the property monitors, for the same property file but different test bench circuits.
Table 9.1
|Test Bench |Ts(in s) without monitors|Ts(in s) with monitors |Batt_Cap(in Amp-hrs) |
|TB1 | 22 |30 |0.1 |
|TB2 | 20 |23 |0.5 |
|TB3 |20 |22 |0.5 |
The property file that we are using contains the properties P1,P3 and P4 of the battery charger that are listed in the Appendix and a false property which should fail for the design.
TB1 : The first test bench is written for a full charge-cycle simulation. Battery capacitor was reduced so that charging takes place quickly.
TB2 : From snapshot shown in the Fig.9.1 we see that except the false property all other properties were vacuously true. For example, the state pre-charge was not reachable in the previous run due to lower value of BATT_CAP. In this test bench we forced the fsm to pre-charge.
TB3 : In this test bench the charger was forced into maintenance mode. We wanted to check whether it returned to full_rate mode when enabling conditions hold on the analog signals.
Fig 9.1 shows the run for TB1 where only the false property failed and all other properties matched vacuously.
Fig 9.2 shows the instantiation of as many as six monitors in the test bench. Note the two current monitors were to be placed between the same two electrical ports and hence they had to be placed in series.
[pic]
Fig. 9.1 : Snapshot of the dynamic ABV report for a sample run
[pic]
Fig. 9.2. Snapshot of the test bench after the instantiation of the monitors
Results could have been taken in other forms as well.
For example, we could give the break-up of the time spent at different phases of the run of the tool : generation of monitors, generation of SVA file and dummy module from the AMS_SVA and test bench files, instantiation of the monitors etc. and thereby determine the bottleneck in the tool.
These results can be easily obtained because our tool has the feature of executing in a step by step manner besides executing in one-go.
Generating such results is not really the aim of the project. We have already seen that the real simulation overhead for these monitors would be negligible when the simulation time would be huge, which is actually the norm in industries.
So far we have tried on simple but representative designs, namely an arbiter circuit (with no analog part),a LCR circuit(where rise time properties were checked) and the battery charger(where several analog properties could be checked).
9.2 Conclusion
We have presented a novel methodology for the verification of mixed signal designs. We believe that the tool produced has the potential to meet the industry requirements. Specially, when there is no such existing tool in the industry, the work could be rated as a brave attempt and an effective one too.
9.3 Future work
The main task ahead is trying this tool on large industrial designs and then assessing its performance. We are of the opinion that for small designs it should do quite well.
In future, we can make our AMS_SVA language more rich by incorporating extra features. Presently, it does not support the use of local variables and multiple clock expressions.
-----------------------
Specification
Implementation
Formal Checker
YES
NO
GenANALOG_monitors
(Generates Verilog AMS monitors for the analog events)
GenSVA_ANALOG_assertions
(Replaces the analog blocks by Boolean variables)
AMS_SVA Assertions
Simulation Engine
TEST BENCH
DUT
Dynamic ABV report
SVA property files
Dummy Verilog module
I
N
T
E
R
F
A
C
E
pipe
VPI
SVDPI
CADENCE
Environment
SYNOPSIS
Environment
................
................
In order to avoid copyright disputes, this page is only a partial summary.
To fulfill the demand for quickly locating and searching documents.
It is intelligent file search solution for home and business.
Related searches
- getroman com reviews
- acurafinancialservices.com account management
- acurafinancialservices.com account ma
- getroman.com tv
- http cashier.95516.com bing
- http cashier.95516.com bingprivacy notice.pdf
- connected mcgraw hill com lausd
- education.com games play
- rushmorelm.com one time payment
- autotrader.com used cars
- b com 2nd year syllabus
- gmail.com sign in