A. W. Appel, Modern compiler implementation in ML, 1998.
DOI : 10.1017/CBO9780511811449

]. I. Bbde-+-01, S. Beer, C. Ben-david, D. Eisner, A. Fisman et al., The temporal logic sugar, 13th International Conference on Computer Aided Verification (CAV'01), volume 2102 of Lecture Notes in Computer Science, pp.363-367, 2001.

. Bbl-+-01-]-f, J. R. Balarin, L. Burch, Y. Lavagno, R. Watanabe et al., Constraints specification at higher levels of abstraction, Proceedings of the IEEE International High Level Design Validation and Test Workshop (HLDVT'01), 2001.

]. A. Bcc-+-99, A. Biere, E. M. Cimatti, M. Clarke, Y. Fujita et al., Symbolic model checking using SAT procedure instead of BDDs, Proceedings of the 36th Design Automation Conference (DAC'99), pp.317-320, 1999.

]. B. Bcc-+-03, P. Blanchet, R. Cousot, J. Cousot, L. Feret et al., A static analyzer for large safety-critical software, Conference on Programming Language Design and Implementation (PLDI'03), pp.196-207, 2003.

. R. Bcl-+-94-]-j, E. M. Burch, D. E. Clarke, K. L. Long, D. L. Mcmillan et al., Symbolic model checking for sequential circuit verification, IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol.13, issue.4, pp.401-424, 1994.

L. [. Breuer, C. D. Fernández, F. Kloos, Y. Balarin, H. Watanabe et al., Clean formal semantics for VHDL Metropolis: An integrated electronic system design environment, The European Conference on Design, pp.45-52, 2003.

A. [. Clarke, R. Biere, Y. Raimi, and . Zhu, Bounded model checking using satisfiability solving, Formal Methods in System Design, vol.19, issue.1, pp.7-34, 2001.
DOI : 10.1023/A:1011276507260

R. [. Cousot and . Cousot, Abstract interpretation, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages , POPL '77, pp.238-252, 1977.
DOI : 10.1145/512950.512973

URL : https://hal.archives-ouvertes.fr/inria-00528590

]. P. Cc79a, R. Cousot, and . Cousot, Constructive versions of Tarski's fixed point theorems, Pacific Journal of Mathematics, vol.81, issue.1, pp.43-57, 1979.

]. P. Cc79b, R. Cousot, and . Cousot, Systematic design of program analysis frameworks, Conference Record of the 6th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp.269-282, 1979.

R. [. Cousot and . Cousot, Abstract Interpretation Frameworks, Journal of Logic and Computation, vol.2, issue.4, pp.511-547, 1992.
DOI : 10.1093/logcom/2.4.511

E. [. Clarke and . Emerson, Design and synthesis of synchronization skeletons using branching time temporal logic, Proceedings of the Workshop on Logics of Programs, pp.52-71, 1981.
DOI : 10.1007/BFb0025774

E. [. Clarke, A. P. Emerson, and . Sistla, Automatic verification of finite state concurrent system using temporal logic specifications, Proceedings of the 10th ACM SIGACT-SIGPLAN symposium on Principles of programming languages , POPL '83, 1983.
DOI : 10.1145/567067.567080

N. [. Cousot and . Halbwachs, Automatic discovery of linear restraints among variables of a program, Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages , POPL '78, 1978.
DOI : 10.1145/512760.512770

]. Cho99, . M. Chou-[-cky03-]-e, D. Clarke, K. Kroening, and . Yorav, The mathematical foundation of symbolic trajectory evaluation Behavioral consistency of C and verilog programs using bounded model checking, 11th International Conference on Computer Aided Verification (CAV'99), volume 1633 of Lecture Notes in Computer Science Proceedings of the 40th Design Automation Conference (DAC'03), pp.196-207, 1999.

P. [. Ciesielski, Z. Kalla, B. Zeng, and . Rouzeyre, Taylor expansion diagrams: a compact, canonical representation with applications to symbolic verification, Proceedings 2002 Design, Automation and Test in Europe Conference and Exhibition, pp.285-291, 2002.
DOI : 10.1109/DATE.2002.998286

URL : https://hal.archives-ouvertes.fr/lirmm-00268497

G. Mathys, A. L. Placido, L. Rosa, and . Lavagno, High-level architectural co-simulation using Esterel and C, Proceedings of the 9th International Symposium on Hardware/Software Codesign (CODES'01), pp.189-194, 2001.

]. P. Cou78 and . Cousot, Méthodes itératives de construction et d'approximation de points fixes d'opérateurs monotones sur un treillis, analyse sémantique de programmes Semantic foundations of program analysis, Cou81] P. Cousot Program Flow Analysis: Theory and Applications, chapter 10, pp.303-342, 1978.

]. P. Cou99 and . Cousot, The calculational design of a generic abstract interpreter, Calculational System Design. NATO ASI Series F. IOS Press, 1999.

D. [. Déharbe and . Borrione, A qualitative finite subset of VHDL and semantics, 1993.

D. [. Déharbe, . [. Borrione, D. Dushina, and . Borrione, Semantics of a verification-oriented subset of VHDL, Correct Hardware Design and Verification Methods (CHARME'95) 2nd Workshop on Libraries, Component Modeling and Quality Assurance, pp.293-310, 1995.
DOI : 10.1007/3-540-60385-9_18

. A. Dbb-+-02-]-j, R. A. Darringer, S. Bergamaschi, D. Bhattacharya, A. Brand et al., Early analysis tools for System-on-a-chip design, IBM Journal of Research and Development, issue.6, pp.46691-707, 2002.

]. E. Dij75 and . Dijkstra, Guarded commands, nondeterminacy and formal derivation of programs, Communications of the ACM, vol.18, issue.8, pp.453-457, 1975.

R. [. Damas and . Milner, Principal type-schemes for functional programs, Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '82, pp.207-212, 1982.
DOI : 10.1145/582153.582176

H. [. Davis and . Putnam, A Computing Procedure for Quantification Theory, Journal of the ACM, vol.7, issue.3, pp.201-215, 1960.
DOI : 10.1145/321033.321034

S. [. Déharbe, E. M. Shankar, and . Clarke, Model Checking VHDL with CV, Proceedings of the 2nd International Conference on Formal Methods in Computer-Aided Design (FM- CAD'98, pp.508-514, 1998.
DOI : 10.1007/3-540-49519-3_33

[. Eia, Electronic Industries Association) Electronic Design Interchange Format (EDIF) Version 3 0 0 Level 0 Reference Manual, 1993.

]. E. Enc95 and . Encrenaz, A symbolic relation for a subset of VHDL'87 descriptions and its application to symbolic model checking, Correct Hardware Design and Verification Methods (CHARME'95), pp.328-342, 1995.

]. J. Fer01 and . Feret, Abstract interpretation-based static analysis of mobile ambients, Static Analysis Symposium (SAS'01), pp.412-430, 2001.

]. J. Fer04, M. Feret, and . Mendler, Static analysis of digital filters Functional semantics for deltadelay VHDL based on focus, 13th European Symposium on Programming Formal Semantics for VHDL, pp.33-48, 1995.

]. H. Fos02, ]. A. Fostergb03, R. E. Goel, and . Bryant, Unifying traditional and formal verification through property checking Set manipulation with boolean functional vectors for symbolic reachability analysis, Designing Correct Circuits Design , Automation and Test in Europe Conference and Exposition (DATE'03), pp.10816-10821, 2002.

R. [. Goel and . Bryant, Symbolic simulation, model checking and abstraction with partially ordered boolean function vectors, Computer-Aided Verification, 2004.
DOI : 10.1007/978-3-540-27813-9_20

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=

D. [. Georgelin, P. Borrione, and . Ostier, A framework for VHDL combining theorem proving and symbolic simulation, Proceedings of the 3rd International Workshop on the ACL2 Theorem Prover and its Applications (ACL2'02), pp.6-14, 2002.
URL : https://hal.archives-ouvertes.fr/hal-01375425

]. D. Gol94 and . Goldschlag, A formal model of several fundamental VHDL concepts, Proceedings of the 9th Annual Conference on Computer Assurance (COMPASS'94), pp.177-181, 1994.

]. K. Goo95, . J. Goossensgor95-]-m, and . Gordon, Reasoning about VHDL using operational and observational semantics The semantic challenge of verilog HDL, Correct Hardware Design and Verification Methods (CHARME'95) Proceedings of the 10th Annual IEEE Symposium on Logic in Computer Science (LICS'95), pp.311-327, 1995.

]. P. Gra91, . Grangergra92-]-p, and . Granger, Static analysis of linear congruence equalities among variables of a program Improving the results of static analyses programs by local decreasing iteration, Proceedings of the International Joint Conference on Theory and Practice of Software Development (TAPSOFT'91 Foundations of Software Technology and Theoretical Computer Science (FSTTCS'92), pp.169-192, 1991.

. Gro96, V. The, and . Group, Vis: A system for verification and synthesis, 8th International Conference on Computer Aided Verification (CAV'96), pp.428-432, 1996.

A. [. Horwitz, T. Demers, and . Teitelbaum, An efficient general iterative algorithm for dataflow analysis, Acta Informatica, vol.24, issue.6, pp.679-694, 1987.
DOI : 10.1007/BF00282621

A. [. Howe and . King, Positive Boolean Functions as Multiheaded Clauses, 17th International Conference in Logic Programming (ICLP'01), pp.120-134, 2001.
DOI : 10.1007/3-540-45635-X_16

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=

E. [. Hymans and . Upton, Static Analysis of Gated Data Dependence Graphs, 11th International Static Analysis Symposium, 2003.
DOI : 10.1007/978-3-540-27864-1_16

]. C. Hym02a and . Hymans, Checking safety properties of behavioral VHDL descriptions by abstract interpretation, 9th International Static Analysis Symposium (SAS'02), volume 2477 of Lecture Notes in Computer Science, 2002.

]. C. Hym02b and . Hymans, Modular analysis of circuit description language by abstract interpretation: Application to the automatic extraction of circuit shapes, Designing Correct Circuits (DCC'02, 2002.

. Int03 and S. International, International Technology Roadmap for Semiconductors Available at: http://public.itrs, 2003.

]. A. Jai97, S. W. Jain, and . Jones, Formal hardware verification by symbolic trajectory evaluation Exponential trends in the integrated circuit industry, 1997.

]. M. Kar76 and . Karr, Affine relationships among variables of a program, Acta Informatica, vol.6, 1976.

]. G. Kil73, A unified approach to global program optimization, 1st ACM Symposium on Principles of Programming Languages, pp.194-206, 1973.

J. [. Kölbl, R. F. Kukula, and . Damiano, Symbolic RTL simulation, Proceedings of the 38th conference on Design automation , DAC '01, pp.47-52, 2001.
DOI : 10.1145/378239.378278

]. S. Kle52 and . Kleene, Introduction to Metamathematics, 1952.

J. [. Lohse, M. Bormann, G. Payer, and . Venzl, VHDLtranslation for BDD-based formal verification, 1994.

]. X. Ldg-+-02, D. Leroy, J. Doliguez, D. Garrigue, J. Rémy et al., The Objective Caml system release 3.06, documentation and user's manual, Institut National de Recherche en Informatique et en Automatique (INRIA), 2002.

A. [. Lichtenstein and . Pnueli, Checking that finite state concurrent programs satisfy their linear specification, Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on Principles of programming languages , POPL '85, 1985.
DOI : 10.1145/318593.318622

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=

]. L. Mau94 and . Mauborgne, Abstract interpretation using TDGs, Static Analysis Symposium, pp.363-379, 1994.

E. [. Müller, U. Börger, and . Glässer, The semantics of behavioral VHDL'93 descriptions, Proceedings of the European Design Automation Conference (EURO-DAC'94), pp.500-505, 1994.

A. [. Mathys and . Chátelain, Verification strategy for integration 3G baseband SoC, Proceedings of the 40th conference on Design automation , DAC '03, pp.7-10, 2003.
DOI : 10.1145/775832.775835

J. [. Modi and . Cortadella, Boolean decomposition using twoliteral divisors, 17th International Conference on VLSI Design (VLSI Design 2004), pp.765-768, 2004.

[. Medea+, Microelectronics Development for European Applications ) Design Automation Solutions for Europe, 2002.

]. R. Mil90 and . Milner, Operational and algebraic semantics of concurrent processes In Handbook of Theoretical Computer Science, volume B: Formal Models and Semantics, pp.1201-1242, 1990.

]. A. Min01 and . Miné, A new numerical abstract domain based on difference-bound matrices, Programs as Data Objects (PADO'02), pp.155-172, 2001.

]. A. Min02 and . Miné, A few graph-based relational numerical abstract domains, Static Analysis Symposium (SAS'02), pp.117-132, 2002.

Y. Madigan, L. Zhao, S. Zhang, and . Malik, Chaff: Engineering an efficient SAT solver, Proceedings of the 38th Design Automation Conference (DAC'01, 2001.

P. [. Magarshack and . Paulin, System-on-chip beyond the nanometer wall, Proceedings of the 40th conference on Design automation , DAC '03, pp.419-424, 2003.
DOI : 10.1145/775832.775943

]. G. Plo81 and . Plotkin, A structural approach to operational semantics, 1981.

]. A. Pnu77 and . Pnueli, The temporal logic of programs, 18th IEEE Symposium on Foundations of Computer Science, pp.46-57, 1977.

D. [. Rodríguez-carbonell and . Kapur, An Abstract Interpretation Approach for Automatic Generation of Polynomial Invariants, 11th Static Analysis Symposium (SAS'04), Lecture Notes in Computer Science, 2004.
DOI : 10.1007/978-3-540-27864-1_21

G. [. Reed and . Solomon, Polynomial Codes Over Certain Finite Fields, Journal of the Society for Industrial and Applied Mathematics, vol.8, issue.2, pp.300-304, 1960.
DOI : 10.1137/0108018

]. D. Rus95a and . Russinoff, A formalization of a subset of VHDL in the Boyer-Moore logic. Formal Methods in System Design, pp.7-25, 1995.

]. D. Rus95b and . Russinoff, Specification and verification of gate-level VHDL models of synchronous and asynchronous circuits, 1995.

[. H. Seger and R. E. Bryant, Formal verification by symbolic evaluation of partially-ordered trajectories, Formal Methods in System Design, vol.6, issue.No. 5, pp.147-189, 1995.
DOI : 10.1007/BF01383966

. A. Skh02, A. Simon, J. M. King, and . Howe, Two variables per linear inequality as an abstract domain, Logic Based Program Synthesis and Tranformation (LOPSTR'02), pp.71-89, 2002.

A. [. Sharp and . Mycroft, A Higher-Level Language for Hardware Synthesis, Correct Hardware Design and Verification Methods, pp.228-243, 2001.
DOI : 10.1007/3-540-44798-9_20

H. [. Sankaranarayanan, Z. Sipma, and . Manna, Non-linear loop invariant generation using gröbner bases, Proceedings of the 31st Symposium on Principles of Programming Languages (POPL'04), pp.318-329, 2004.

S. [. Sheeran, G. Singh, and . Stålmarck, Checking Safety Properties Using Induction and a SAT-Solver, 3rd International Conference On Formal Methods in Computer Aided Design (FMCAD'00), volume 1954 of Lecture Notes in Computer Science, 2000.
DOI : 10.1007/3-540-40922-X_8

M. [. Stewart and . Vaninwegen, Three notes on the interpretation of verilog, 2000.

]. J. Tas93 and . Van-tassel, FEMTO-VHDL: The semantics of a subset of VHDL and its embedding in the hol proof assistant, 1993.

R. [. Thirunarayan and . Ewing, Structural operational semantics for a portable subset of behavioral VHDL-93. Formal Methods in System Design, pp.69-88, 2001.

]. P. Van-der-wolf, P. Lieverse, M. Goel, and D. L. Hei, An MPEG-2 decoder case study as a driver for a system level design methodology, Proceedings of the seventh international workshop on Hardware/software codesign , CODES '99, 1999.
DOI : 10.1145/301177.301196

P. [. Vardi and . Wolper, An automata-theoretic approach to automatic program verification, 1st Annual Symposium on Logic in Computer Science (LICS'86), 1986.
DOI : 10.1007/3-540-50403-6_33

D. [. Wilson, R. E. Dill, and . Bryant, Symbolic Simulation with Approximate Values, Formal Methods in Computer- Aided Design, pp.470-485, 1954.
DOI : 10.1007/3-540-40922-X_29

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=

D. [. Wilhelm and . Maurer, Compiler design, 1995.
DOI : 10.1007/978-3-642-17540-4

]. K. Yi01 and . Yi, Yet another ensemble of abstract interpreter, higherorder data-flow equations, and model checking, 2001.