Drechsler - Formal System Verification: State-of the-Art and Future Trends
Here you can read online Drechsler - Formal System Verification: State-of the-Art and Future Trends full text of the book (entire story) in english for free. Download pdf and epub, get meaning, cover and reviews about this ebook. City: Cham, year: 2018, publisher: Springer International Publishing : Imprint : Springer, genre: Computer. Description of the work, (preface) as well as reviews are available. Best literature library LitArk.com created for fans of good reading and offers a wide selection of genres:
Romance novel
Science fiction
Adventure
Detective
Science
History
Home and family
Prose
Art
Politics
Computer
Non-fiction
Religion
Business
Children
Humor
Choose a favorite category and find really read worthwhile books. Enjoy immersion in the world of imagination, feel the emotions of the characters or learn something new for yourself, make an fascinating discovery.
Formal System Verification: State-of the-Art and Future Trends: summary, description and annotation
We offer to read an annotation, description, summary or preface (depends on what the author of the book "Formal System Verification: State-of the-Art and Future Trends" wrote himself). If you haven't found the necessary information about the book — write in the comments, we will try to find it.
Formal Techniques for Verification and Coverage Analysis of Analog Systems -- Verification of Incomplete Designs -- Probabilistic Model Checking: Advances and Applications -- Software in a Hardware View -- Formal Verification -- The Industrial Perspective.;This book provides readers with a comprehensive introduction to the formal verification of hardware and software. World-leading experts from the domain of formal proof techniques show the latest developments starting from electronic system level (ESL) descriptions down to the register transfer level (RTL). The authors demonstrate at different abstraction layers how formal methods can help to ensure functional correctness. Coverage includes the latest academic research results, as well as descriptions of industrial tools and case studies. Provides latest results on formal methods along the complete design flow; Covers different abstraction layers, from ESL to RTL; Addresses formal verification in both digital and analog contexts; Demonstrates techniques in current industrial use.
Drechsler: author's other books
Who wrote Formal System Verification: State-of the-Art and Future Trends? Find out the surname, the name of the author of the book and a list of all author's works by series.
Edmund M. Clarke Jr.
Honghao Gao
Bowen Judith Alyson
Djones Lettnin
Sherief Reda
Formal System Verification: State-of the-Art and Future Trends — read online for free the complete book (whole text) full work
Below is the text of the book, divided by pages. System saving the place of the last page read, allows you to conveniently read the book "Formal System Verification: State-of the-Art and Future Trends" online for free, without having to search again every time where you left off. Put a bookmark, and you can go to the page where you finished reading at any time.
Light
Font size:
↓
↑
Reset
Interval:
↓
↑
Bookmark:
Make
Springer International Publishing AG 2018
Rolf Drechsler (ed.) Formal System Verification 10.1007/978-3-319-57685-5_11. Formal Techniques for Verification and Coverage Analysis of Analog Systems
Andreas Frtig 1
(1)
University of Frankfurt, Frankfurt/Main, Germany
Andreas Frtig (Corresponding author)
Email:
Lars Hedrich
Email:
Andreas Frtig
received the Diploma degree in computer science from the Goethe-University of Frankfurt in 2013. He is currently pursuing as a Ph.D. student at the institute of computer science within the design methodology group supervised by Prof. Dr. L. Hedrich. His current research interests include formal verification methods, simulation and coverage metrics of analog circuits, as well as behavioral modeling. He is also the teamleader of the RoboCup SPL Team Bembelbots.
Lars Hedrich
received the Diploma degree in electrical engineering in 1992 and the Ph.D. from the University of Hannover in 1997 and became a Juniorprofessor at the same University in 2002. Since 2004 he is full professor at the Institute of Computer-Science, University of Frankfurt, and head of the design methodology group at the same institute. His research interests include several areas of analog design automation: symbolic analysis of linear and nonlinear circuits, behavioral modeling, reliability analysis and design, circuit synthesis, and formal verification.
1.1 Introduction
Besides the pure digital and software-related verification methodologies, analog and mixed signal circuits and systems are also in strong focus of adding formal verification into the verification flow. In fact, the validation demand can be higher than in pure digital design because the systems behavior due to the continuous nature of the signals gives more freedom to signal processing. The main driving forces in IC and embedded systems market are communication and automotive circuits. Both demand for substantial analog parts coupled with digital parts. On top of that, these mixed-signal systems are connected with sensors and actors to the physical world in a control loop such that the overall system validation has to take the digital part, the analog part, the sensors, and the physical world into account. The analog parts (around 1030% of the chip area) have fewer transistors (1001000 for a block) and may add up in tens to hundreds of blocks. Clearly, these analog blocks are nonlinear dynamic circuits with the nonlinearity being a major property of the circuit.
The variety of analog circuits directly leads to a large variety of verification methodseven in simulation-based approaches. There are a lot of simulators on many levels of abstraction, starting from device simulators up to system-level design-languages and simulators like SystemC-AMS [].
Unfortunately the analog/continuous circuits do not have a nice Boolean abstraction layer, which paves the way for digital formal verification tools. Hence, the available analog verification tools are more or less focused on the abstraction layer they reside on. Most tools have big complexity issues keeping the size of verifiable circuits small and hence adding more pressure to have dedicated tools for many abstraction layers. Furthermore, this demands for cross abstraction-layer tools like equivalence checking. We will present some ideas to formal verification on transistor level and extend them to close the gap to higher level abstractions.
Another way of increasing the confidence into the designed analog circuitry is the introduction of coverage measures. Depending on the type of coverage, one can get a closed form, well defined, formal coverage definition accompanied by proper algorithms. On the other end, there may be ad hoc methods with created tests from experienced designers having all to be fullfilled to get 100% coverage. In this chapter, we will describe and discuss some methods for analog coverage.
Coming to system level the picture turns into something slightly different. Here, a long tradition of hybrid system formal verification methods exists, which now has to be connected with the lower level circuitry. We will present some methods and their applications and show a way to close the gap down to transistor level using a chain of formal verification steps and a stack of abstracted behavioral models. We will show, how a system-level formal verification could be applied on an example consisting of a cyber-physical system.
This chapter begins with a state-of-the-art section, a description of the analog/continuous state space and its algorithmic handling. We will then discuss several verification methods in Sect. combines all presented methods to apply formal verification to the system level.
1.2 State of the Art
As described in the other chapters of this book, formal verification of digital circuits has a long tradition and is deeply integrated in design companies verification flow. However, for analog circuits or continuous systems on system level a need for accurate and fast verification methods becomes more important as cyber-physical systems and Internet of things produces a lot of sensors, actors, and hence continuous-centric designs.
In any case, the objective of formal verification is to mathematically prove properties of a system, usually at design time. It can be distinguished between reachability analysis, model checking, and more specific equivalence checking. Model checking is mainly used for formally verifying specified properties that in particular relate to safety and liveness of a system. Equivalence checking, being able to prove the equivalence of two implementations could be used to build a chain of proof from lower level implementations up to abstract behavioral models. Reachability analysis is the little friend of model checking, as it allows an easy straightforward way of a safety proof. For hybrid systems on system level, this technique is used the most.
System Level
A first approach to move from discrete systems to continuous systems was based on hybrid automata and eventually evolved in the tool HyTech [] in order to compute reachable sets which can be checked for hitting a forbidden region.
Later, the tools for hybrid systems evolve introducing polyhedra as data structures [].
The used underlying data structures and computation models began to broaden from Petri nets [].
Transistor Level
However, to be more accurate on lower levels of abstraction one has to incorporate the transistor which is really hard to model by piecewise-linear hybrid systemsa todays transistor model consists of hundreds of nonlinear equations. Additionally, the Kirchhoffs laws do not allow solving the nonlinear differential algebraic system (DAE) for getting an explicit ordinary differential equation (ODE) description needed by most hybrid-systems approaches. Consequently, some different methods evolve. One approach extends affine arithmetics with a Newton iteration to solve nonlinear equation systems [].
Other approaches try to abstract the exact nonlinear behavior by determining an analog state transition graph using the original netlist and detailed BSIM transistor models with simulator engines and full SPICE-accuracy [].
Formal Languages
In []. All these methods can be used to model check the design under verification or at least enable an assertion-based verification (ABV) by running in parallel with a simulation. This is a big advantage, as it scales better with netlist size by not exploring the exponential growing state space. The disadvantage is that the proving character will be lost. All these formal language based approaches suffer hard to interpret results and the perennial translate specification into a formal language problem.
Light
Font size:
↓
↑
Reset
Interval:
↓
↑
Bookmark:
Make
Similar books «Formal System Verification: State-of the-Art and Future Trends»
Look at similar books to Formal System Verification: State-of the-Art and Future Trends. We have selected literature similar in name and meaning in the hope of providing readers with more options to find new, interesting, not yet read works.
Edmund M. Clarke Jr.
Honghao Gao
Bowen Judith Alyson
Djones Lettnin
Sherief Reda
Reviews about «Formal System Verification: State-of the-Art and Future Trends»
Discussion, reviews of the book Formal System Verification: State-of the-Art and Future Trends and just readers' own opinions. Leave your comments, write what you think about the work, its meaning or the main characters. Specify what exactly you liked and what you didn't like, and why you think so.