Vérification de descriptions VHDL par interprétation abstraite

Semiconductors

Digital cameras, voice over IP phones, harvester guidance systems, factory monitors, smart rifles, brake controllers and pacemakers, all these devices incorporate integrated circuits. According to [MED04], the market of the semiconductor industry totaled $141 billion in 2003, while the electronic industry addressed a $800 billion market. Are there more tangible proofs of the pervasive influence of semiconductors on our society? Innovation in semiconductors contributes to the evolution of many industrial sectors. For instance electronics equipment amounts for as much as 20% of the production cost of a car.

The formidable proliferation of hardware in the world began not even a century ago. Bell Labs researchers William Shockley, John Bardeen and Walter Brattain created the first transistor in 1947. Schematically , a transistor operates like a switch: when voltage is applied to the gate (G) then the current between the source (S) and the drain (D) flows, otherwise source and drain are disconnected. Transistors constitute the basic blocks of electronic circuits. The ability to integrate a whole circuit on a single silicon wafer was invented a decade later. In 1958, Jack Kilby, while working at Texas Instrument, built the first integrated circuit.

Verification crisis

Unfortunately the integration of numerous transistors on a chip has a high cost. The investment necessary to build a semiconductor manufacturing plant is evaluated in billion dollars. More importantly, the cost of mask sets have reached prohibitive amounts: it exceeds the million dollars for the 90nm technology and almost tops 2 million dollars in 65nm. To offset such high initial investments chips manufactured with the latest technology must be sold in very high volumes [MP03].

Even worse, designs should be error free before they are sent to fabrication: few companies can afford a million dollar re-spin. To ensure the correctness of their designs, engineers use simulation. Simulation accounts for 60% to 70% of the whole development time [MED02]. The number of engineers allocated to simulation outstrips the number of designers. Apparently, this proves not enough since almost as much as 50% of all designs go through more than one spin. The situation is bound to deteriorate as designs grow in size and complexity. Not only must the simulator handle bigger designs, it has to run more test-vectors so as to exercise a substantial fragment of all the behaviors,  Largely because of the limitations of verification, the gap between what can be manufactured and what can be correctly designed quickly expands, According to the International Roadmap for Semiconductors [Int03], the cost of design is the greatest threat to continuation of the semiconductor roadmap. The situation is quickly becoming a crisis. There is a desperate need for new automatic tools that alleviate the task of verification.

Semantics

Very High Scale/Speed Integrated Circuits Hardware Description Language, aka VHDL, is one of the most widely used hardware description languages. In the early 1980s, the US Department of Defense was facing a crisis: its suppliers all had different ways of documenting hardware. Since the documentations were bound to specific manufacturing technology, they were reaching obsolescence very quickly. Needless to say that interoperability was an inextricable nightmare. Hence, VHDL was initially created as a language to describe the behavior of hardware. The ability to simulate descriptions soon became apparent. Finally, logic synthesis tools made the language even more attractive and gave rise to the modern hardware design methodology. In 1987, VHDL was standardized as IEEE Std 1076 [IEE87]. The up-to-date revision is [IEE02]. IEEE standard 1164 [IEE93] adds an important complement to the language: it defines a data-type to allow the manipulation of multi-valued logic signals.

We favored VHDL for its wide acceptance in the industry. We could have equally opted for Verilog [IEE01]. We strongly believe that a similar methodology can be adopted to develop equally efficient verification tools for Verilog. However, the case study, that professional hardware engineers made available to us, was written in VHDL. Today, engineers spend most of their time working with VHDL (or Verilog). Lower level descriptions, i.e. netlists in edif [EIA93] or blif [Uni92] formats, are manipulated mostly by automatic tools. Higher level descriptions are used to evaluate the impact of hardware (and software) architectural decision early in the design cycle [DBB+02]. Performance/cost estimation [CMP+01], early power analysis [BJ03] and sometimes high-level synthesis [SM01] can all be performed at this level. System level languages and tools have not reached maturity yet and still constitute an active field of research. Among others, system level design languages include SystemC used as in the Metropolis framework [BWH+03], Esterel and Time Modeling Language with the Archan approach [MC03], and Kahn Process Networks and C for the SPADE methodology [vdWLGH99].

Intuition for the semantic model

The processes of a mini-VHDL description are run concurrently. Communication between processes happens through a shared memory (the signals) and only at some specific synchronization points. Once all processes are suspended, synchronization occurs: the memory is updated and the activity of some processes is resumed. We call a simulation cycle, the execution of the system between two consecutive synchronization points.

Le rapport de stage ou le pfe est un document d’analyse, de synthèse et d’évaluation de votre apprentissage, c’est pour cela chatpfe.com propose le téléchargement des modèles complet de projet de fin d’étude, rapport de stage, mémoire, pfe, thèse, pour connaître la méthodologie à avoir et savoir comment construire les parties d’un projet de fin d’étude.

Table des matières

1 Introduction
2 Semiconductors
2.1 Verification crisis
2.2 Motivation
2.3 Results
3 Semantics
3.1 Introduction
3.2 Related work
3.3 Syntax
3.4 Intuition for the semantic model
3.5 The kernel
3.6 More data types: integers and aggregates
3.7 Local variables, conversion functions
3.8 Rising edges and clocks
3.9 Remaining statements
3.9.1 Suspension
3.9.2 Alternative
3.9.3 Display
3.10 A benign parallelism
3.11 Discussion
4 Abstract Interpretation
4.1 Collecting semantics
4.2 Abstract Interpretation
4.3 Abstract domain
4.4 Abstract semantics transformer
4.4.1 Expressions
4.4.2 Sequential statements
4.4.3 Abstract simulation algorithm
4.4.4 Semantics transformer
4.5 Example
4.6 Loop unfolding
4.7 Recapitulation
5 Implementation
5.1 Preprocessor
5.2 Abstract simulator
5.3 The back-end: a numerical domain
5.3.1 Boolean affine relationships
5.3.2 Constants
5.3.3 Arrays
5.4 A trial run
6 Reed Solomon error correcting code
6.1 Motivation
6.2 Reed Solomon
6.3 Encoder
6.3.1 Verification harness
6.3.2 Results
6.3.3 Coding style
6.3.4 Combinational processes
6.4 Decoder
6.4.1 Specification
6.4.2 Inlining combinational processes
6.4.3 Debugging
6.4.4 Statistics
6.5 Related work
7 Conclusion

Rapport PFE, mémoire et thèse PDFTélécharger le rapport complet

Télécharger aussi :

Laisser un commentaire

Votre adresse e-mail ne sera pas publiée. Les champs obligatoires sont indiqués avec *