|
2004
|
J. Schmaltz, D. Borrione
"A Functional Approach to the Formal Specification of Networks on Chip"
in Proc. of Formal Methods in Computer-Aided Design (FMCAD'04)
Austin, Texas, USA, November 14-17, 2004. Editors: Alan J. Hu, Andrew K. Martin
Lecture Notes in Computer Science Volume 3312 / 2004, ISBN: 3-540-23738-0.
Abstract in SpringerLink
|
J. Schmaltz, D. Borrione
"A Functional Specification and Validation Model for Networks on Chip in the ACL2 Logic"
Proceedings of the 5th International Workshop on the ACL2 Theorem Prover and its Applications (ACL2'04)
Austin, Texas, September 18-19, 2004, USA.
|
D. Toma, D. Borrione
"Verfication of a cryptographic circuit: SHA-1 using ACL2"
Proceedings of the 5th International Workshop on the ACL2 Theorem Prover and its Applications (ACL2'04)
Austin, Texas, September 18-19, 2004, USA.
|
G. Al Sammane, J. Schmaltz, D. Toma, P. Ostier, D. Borrione
"Theosim: Combining Symbolic Simulation and Theorem Proving for Hardware Verification"
Proc. of the 17th Symposium on Integrated Circuits and System Design (SBCCI'04)
Porto de Galinhas, Pernambuco, Brazil, September 7-11, 2004.
|
D. Toma, A. Perez, D. Borrione, E. Bergeret
"Design of a proven correct SHA circuit"
Proc. 2004 International Conference on Electrical, Electronic and Computer Engineering (ICEEC-04)
Cairo, Egypt, September 5-7, 2004, IEEE Press.
|
G. Al Sammane, J. Schmaltz, D. Borrione
"Formal Verification of On-Chip Networking"
in Proceedings of the 1st International Conference on Information & Communication Technologies: from Theory to Applications (ICTTA'04)
Damascus, Syria, April 19-23, 2004.
|
D. Toma, D. Borrione, G. Al Sammane
"Combining several paradigms for circuit validation and verification"
in Construction and Analysis of Safe, Secure, and Interoperable Smart Devices: International Workshop
CASSIS 2004, Marseille, France, March 10-14, 2004.
Revised Selected Papers, Editors: Gilles Barthe, Lilian Burdy, Marieke Huisman, et al.
Lecture Notes in Computer Science, Volume 3362 / 2005, ISBN: 3-540-24287-2.
Abstract in SpringerLink
|
G. Al Sammane
"Using Mathematica for Modeling, Simulation, and Property Checking of Hardware Systems"
In Wolfram Technology conference 2004.
|
|
2003
|
D. Borrione, M. Boubekeur, L. Mounier, M. Renaudin, A. Sirianni
"Validation of asynchronous circuit specifications using IF/CADP"
Proc. VLSI-SOC'03, Darmstad, Germany, ISBN 3-901882-17-0, Dec. 2003.
|
G. Al Sammane, D. Borrione, P. Ostier, J. Schmaltz, D. Toma
"Constrained Symbolic Simulation with Mathematica and ACL2"
CHARME'03, Italy, 21-24 October 2003.
|
D. Borrione, M. Boubekeur, L. Mounier, M. Renaudin, A. Sirianni
"Modeling CHP descriptions in Labeled Transitions Systems for an efficient formal validation of asynchronous circuit specifications"
Proc FDL'03, Frankfort, Germany, 23-26 September 2003.
|
D. Borrione, J. Schmaltz
"Verification of a parameterized bus architecture using ACL2"
ACL2 Workshop, Boulder, USA, 13-14 July 2003.
|
G. Al Sammane, D. Borrione, P. Ostier, J. Schmaltz, D. Toma
"Combining ACL2 and Mathematica for the Symbolic Simulation of Digital Systems"
ACL2 Workshop, Boulder, USA, 13-14 July 2003.
|
D. Borrione, D. Toma
"SHA Formalization"
ACL2 Workshop, Boulder, USA, 13-14 July 2003.
|
E Dumitrescu, D. Borrione
"Symbolic simulation as a simplifying strategy for SoC verification with symbolic model checking"
Proc. IWSOC2003, Calgary, Canada, July 2003.
|
J. Schmaltz, D. Borrione
"Formalization and verification of the AMBA AHB communication architecture using the ACL2 theorem prover"
Proc. DDECS'03, Poznan, Poland, April 2003.
|
G. Al Sammane, D. Borrione
"Formal validation of high level specification of data path digital circuits by symbolic simulation"
Proc. DDECS'03, Poznan, Poland, April 2003.
|
G. Al Sammane, D. Borrione
"Design and Verification of Digital Circuits in Mathematica: Symbolic simulation of VHDL descriptions"
2003 Mathematica Developer Conference, April 2003.
|
D. Borrione, M. Boubekeur, E. Dumitrescu, M. Renaudin, J.-B. Rigaud, A. Sirianni
"An approach to the introduction of formal validation in an asynchronous circuit design flow"
Proc. 36B0 HawaC/ International Conference on Systems Science, HawaC/, USA,IEEE Publ., January 6-9, 2003.
|
|
2002
|
D. Borrione
"Formal Verification Tutorial"
invited talk, Proc. MEDEA+ Design Automation Conference, Stresa, Italie, October 23-25, 2002.
|
E. Dumitrescu
"A practical approach to the formal verification of SoCs with symbolic model checking"
Publ. in International Workshop on System On Chip for Real-time Applications (IWSOC'02), Banff, Canada, July 5-7, 2002.
|
J. Vidal, D. DC)harbe, D. Borrione
"Improving static ordering of BDDs for reachability analysis"
Proc. 11th IEEE/ACM International Workshop On Logic & Synthesis (IWLS 02), New Orleans, Louisiana June 4-7, 2002.
|
D. Borrione, M. Boubekeur, E. Dumitrescu, M. Renaudin, J.-B. Rigaud, A. Sirianni
"Introducing formal validation in an asynchronous circuit design flow"
The Fourth International Workshop on Designing Correct Circuits, Grenoble, France, 6-7 April 2002.
|
P. Georgelin, D. Borrione, P. Ostier
"A framework for VHDL combining theorem proving and symbolic simulation"
Proc. third International Workshop on the ACL2 Theorem Prover and its Applications (ACL2'02), Grenoble, France, 6-14 April 2002.
|
D. Borrione
"La simulation et les mC)thodes de vC)rification formelles"
in "Conception de haut niveau des systC(mes monopuces", ed. A. JERRAYA, coll. Electronique GC)nie Electrique MicrosystC(mes , Hermes, 2002, ISBN 2-7462-0433-9.
|
|
2001
P. Georgelin
"VC)rification formelle de systC(mes digitaux synchrones, basC)e sur la simulation symbolique"
PhD Thesis, UniversitC) Joseph Fourier, 18 Octobre 2001.
pdf file.
|
G. Al Sammane
"VC)rification de modC(les de descriptions de haut niveau C)crits en langage SpecC"
Master Thesis, UniversitC) Joseph Fourier, 4 Septembre 2001.
pdf file.
|
D. Borrione
"On the Development of Hardware Description Languages"
Invited paper at the Wissenschaftliches Kolloquium of the Braunschweigische Wissenschaftliche Gesellschaft in the honor of Professor Robert Piloty, Braunschweig, Allemagne, May 18, 2001.
|
S. Reda, A. Wahba, A. Salem, D. Borrione, A. Ghonaimy
"On the Use of Don't Cares during Symbolic Reachability Analysis"
Proc. IEEE Internat. Symposium on Circuits and Systems, Sydney, Australia, May 6-9, 2001.
|
G. Ritter
"Formal sequential equivalence checking of digital systems by symbolic simulation"
ThC(se de Doctorat UJF, SpC)cialitC) MicroC)lectronique, bi-national degree Darmstadt Univ. of Technology, Germany, 26 Mar 2001.
Abstract.
|
D. Borrione, P. Georgelin, V.M. Rodrigues
"Symbolic Simulation and Verification of VHDL with ACL2"
in System-on-Chip Methodologies and Design Languages,
Kluwer Academic Publishers, 2001.
|
D. Borrione, P. Georgelin
"Formal Verification of VHDL using VHDL-like ACL2 models"
in Electronic Chips and Systems Design Languages,
Kluwer Academic Publishers, 2001.
|
|
2000
D. Borrione, J. Dushina, L. Pierre
"A Compositional Model for the Functional Verification of High-Level Synthesis Results"
IEEE Trans. on VLSI Systems, Vol.8, NB05, Oct. 2000.
|
V.M. Rodrigues, D. Borrione, P. Georgelin
"Raisonning about VHDL components with ACL2"
Workshop on Formal Methods (WMF'00), SOCIEDADE BRASILEIRA DE COMPUTACAO, Joao Pessoa, Paràba, Brazil, October 2-4,2000.
|
A. Morawiec
"AmC)lioration de performance de la simulation des modC(les dC)crits en langages de description de matC)riel"
PhD Thesis, UniversitC) Joseph Fourier, 2000.
|
V.M. Rodrigues, D. Borrione, P. Georgelin
"Using the ACL2 theorem prover to Reason about VHDL Components"
in RITA Journal, Volume VII, Numero 1, Universidade Federal do Rio Grande do Sul, Brazil, September 2000.
|
V.M. Rodrigues, D. Borrione, P. Georgelin
"An ACL2 Model of VHDL for Symbolic Simulation and Formal Verification"
in XIII Symposium on Integrated Circuits and Systems Design (SBCCI'00), Manaus, Amazonas, Brazil, September 18-22, 2000.
IEEE Computer Society Press.
|
A. Morawiec, J. Mermet
"Behavioral Abstraction of HDL Models for Simulation Performance"
Asia-Pacific Conference on Chip Design Languages APChDL2000 at 16th IFIP World Computer Congress 2000, Beijing, China, August 21-24, 2000.
|
P. Georgelin, L. Pierre, T. Nguyen
"A Formal Approach for the Specification of Communications in Distributed Systems"
International Conference on Parallel and Distributed Computing Systems (PDCS'2000), Las Vegas, Nevada, August 8-10, 2000.
|
R. Ubar, J. Raik, A. Morawiec
"High-Level Decision Diagrams for Improving Simulation Performance of Digital Systems"
The 4th World Multiconference on Systemics, Cybernetics and Informatics SCI'2000, Orlando, Florida, USA, July, 23-26, 2000.
|
D. Borrione, P. Georgelin, V.M. Rodrigues
"Using macros to mimic VHDL in ACL2"
In M. Kaufmann, P. Manolios, J Moore ed., Computer-Aided Reasoning: ACL2 Case Studies, pp 162-185, Kluwer Academic Publishers, June, 2000.
(ISBN 0-7923-7849-0).
|
R. Ubar, A. Morawiec, J. Raik
"Back-Tracing and Event-Driven Techniques in High-Level Simulation with Decision Diagrams"
2000 IEEE International Symposium on Circuits and Systems ISCAS'2000, Geneva, Switzerland, May 28-31, 2000.
|
R. Ubar, A. Morawiec, J. Raik
"Vector Decision Diagrams for Simulation of Digital Systems"
Design and Diagnostics of Electronic Circuits and Systems Workshop DDECS2000, pp. 44-5, Smolenice, Slovakia, April 5-7, 2000.
|
A. Morawiec, R. Ubar, J. Raik
"Cycle-Based Simulation Algorithms for Digital Systems Using High-Level Decision Diagrams"
DATE 2000, Paris, France, March 27-30, 2000.
|
D. Borrione, P. Georgelin, V.M. Rodrigues
"Symbolic Simulation and Verification of VHDL with ACL2"
HDLCON'2000, San Jose, California, USA, March 8-10 2000.
|
D. Borrione
"Utilisation des méthodes formelles pour la vérification des
systèmes intégrés digitaux"
Conférence invitée, AFADL'2000, Grenoble, 26-28 janvier 2000.
|
J. Mermet
"Les langages pour la conception des circuits intégrés"
Techniques de l'ingénieur, (60p), 2000.
|
|
1999
|
UBAR R., BORRIONE D.
Design Error Diagnosis in Digital Circuits without Error Model
Proc. IFIP International Conference: VLSI'99, Lisbonne, Portugal, Dec 1-4, 1999 Kluwer Academic Publishers, pp. 281-292.
|
DUSHINA J.
Vérification formelle des résultats de la Synthese de Haut Niveau
(Formal Verification of high level synthesis results)
To satisfy the present market requirements, several commercial formal
verification tools appeared recently. The highest description level accepted by
these tools is the so-called Register Transfer Level, i.e. with clearly
identified clock periods. Because of very strong competition the designers must,
however, start from more abstract initial descriptions and use high-level
synthesis tools. This thesis addresses the formal verification of high-level
synthesis results with respect to the initial specification given in VHDL. We
propose a methodology that follows the design flow and includes the verification
of two main synthesis steps: scheduling and allocation. The verification of each
step is based on an abstract machine model that we developed: contrary to the
classic finite state machine, it reduces considerably the state space by keeping
the data path registers symbolic. Moreover, the similarity between the abstract
machine and the VHDL description provides facilities for the model construction
and understanding. The proof of the equivalence between abstract and classical
finite state machines justifies the abstract machine and constitutes one of the
theoretical contributions of the thesis. A prototype tool based on symbolic
execution was developed and applied to some high-level synthesis benchmarks.
Finally, the thesis points out some open problems and suggests some research
directions to solve them.
PhD thesis, October 27,1999, UJF.
|
BORRIONE D., GEORGELIN Ph.
Formal Verification of VHDL Using VHDL-like ACL2 Models
When a design reaches the register transfer level, essential architectural
decisions have been taken; their validation required extensive simulation of the
abstract behavioral specifications. The recognized need for formal verification
cannot be met by current automatic equivalence and model checking tools, which
mainly apply to logic synthesis inputs and outputs, or require manual
abstraction. We propose to introduce mechanically supported formal reasoning in
the design flow, by producing a model of VHDL behavioral specifications in the
logic of the ACL2 theorem prover. Written in Lisp, this model is executable as
well as subject to symbolic manipulations. We define the semantics of VHDL data
types and behavioral-style statements in the logic. We use macros to generate
names, function definitions and theorems automatically, by instantiation of
model skeletons, while retaining an algorithmic syntactic flavor. This feature
is particularly useful to translate VHDL statements into resembling ACL2 macros,
so that the logic formalization remains readable.
Proc. Forum on Design Languages 1999, Lyon, August 30-September 3, 1999.
|
MORAWIEC A., MERMET J.
Techniques for Improving the HDL Simulation Performance
Paper and poster at Forum on Design Languages FDL'99, August 30-September 3, 1999, Lyon, France (Best Poster Award).
|
UBAR R.*, BORRIONE D.
Design Error Diagnosis in Digital Circuits without Error Model
We describe a new method for design error diagnosis in digital circuits, that
doesn't use any error model. A diagnostic specific pre-analysis of the circuit
extracts a subcircuit suspected to be erroneous. Contrary to other published
works, here the necessary re-synthesis of the subcircuit need not be applied to
the whole function of an internal signal in terms of primary inputs, but may
stop at arbitrary nodes inside the circuit. As the subcircuits to be redesigned
are kept as small as possible, the redesign procedure is simple and fast.
Experimental data also show the high speed of the diagnostic pre-analysis.
TIMA Research Report, 14 June 1999.
Pdf file.
*Tallinn Technical University, Raja 15, EE0026 Tallinn, Estonia.
|
MORAWIEC A., MERMET J.
Methodes pour l'amelioration de la performance de simulation
Colloque CAO de circuits integres et systemes, May 10-12, 1999, Fuveau, France.
|
GEORGELIN Ph.
Symbolic Simulation and proofs of VHDL descriptions with the ACL2 theorem prover (in French)
Colloque CAO de circuits integres et systemes, May 10-12, 1999, Fuveau, France.
|
UBAR R., MORAWIEC A., RAIK J.
Cycle-based Simulation with Decision Diagrams
DATE'99 Conference, March 9-12 1999, Munich, Germany, pp. 454-458.
|
BORRIONE D., ERNST R. Editeurs
Design Automation and Test in Europe - DATE'99
Proceedings International Conference, Munich, Germany, March 99, IEEE CS Press, ISBN 0-7695-0078-1.
|
|
|
1998
MERMET J., Guest editor
Special issue of the Journal of Electrical Engineering and Information Science.
6 Dec. 1998 "3 decades of hardware description languages in Europe".
|
MERMET J.
CASSANDRE: a language for Computer Aided Simulation and Synthesis Analysis Description and Realisation of digital systems (in *)
|
BORRIONE D., LE FAOU C., MERMET J.
CASCADE (in *)
|
MERMET J., MARWEDEL P., RAMMING F., NEWTON C., BORRIONE D., LE FAOU C.
Three Decades of Hardware Description Languages in Europe
Journal of Electrical Engineering and Information Science, Vol.3, N 6, 1998.
|
DUMITRESCU E., OSTIER P.
Identification of non-redundant memorizing elements in VHDL synchronous designs for formal verification tools
|
UBAR R.*, BORRIONE D.
Generation of Tests for the Localization of Single Gate Design Errors in Combinational Circuits Using the Stuck-at Fault Model
We propose a new approach to generate diagnostic tests and localize single
gate design errors in combinational circuits. The method is based on using the
stuck-at fault model with subsequent translation of the diagnosis into the
design error area. This allows to exploit standard gate-level ATPGs for
verification and design error diagnosis purposes.
A powerful hierarchical approach is proposed for generating test patterns which,
at first, localize the faulty macro (tree-like subcircuit), and then localize
the erroneous gate in the faulty macro. Experimental data show the efficiency of
the macro-level test generation and fault simulation compared to the plain
gate-level approaches.
XI Brazilian Symposium on Integrated Circuit Design, Buzios, Brasil, September 30-October 3, 1998.
Postscript file.
*Tallinn Technical University, Raja 15, EE0026 Tallinn, Estonia.
|
BORRIONE D., DUSHINA J., PIERRE L.
Formalization of Finite State Machines with Data Path for the Verification of High-Level Synthesis
XI Brazilian Symposium on Integrated Circuit Design, Buzios, Brasil, September 30-October 3, 1998.
Postscript file.
|
DUSHINA J., BORRIONE D., JERRAYA A.
Formal Verification of the Allocation Step in High Level Synthesis
This paper addresses the problem of verifying the correctness of high level
synthesis results with respect to their initial behavioral specification. We
propose to perform the verification in the same two major steps as the High
Level Synthesis process: scheduling and allocation. This article is devoted to
the allocation step. Two formal models, corresponding to the synthesized circuit
before and after allocation, are developed. Compared to classical Finite State
Machines, they provide a significant reduction of the state space by keeping the
data path registers symbolic, and using algebraic expressions for the functional
behaviour. The algebraic expressions of the model after allocation are
automatically constructed by symbolic execution of the synthesis results. The
article explains the principles of the verification prototype tool.
Forum on Design Languages (FDL'98), Lausanne, Switzerland, September 6-11, 1998.
Postscript file.
|
UBAR R.*, BORRIONE D.
Localization of single gate design errors in combinational circuits by diagnostic information about stuck-at faults
Design and Diagnostics of Electronic Circuits and Systems Workshop (DDECS'98), Szczyrk, Poland, 2-4 September 1998.
Pdf file.
*Tallinn Technical University, Raja 15, EE0026 Tallinn, Estonia.
|
UBAR R.*, BORRIONE D.
Generation of Tests for the Localization of Single Gate Design Errors in Combinational Circuits Using the Stuck-at Fault Model
Research Report, TIMA, INPG, Grenoble, France, May 1998.
Pdf file.
*Tallinn Technical University, Raja 15, EE0026 Tallinn, Estonia.
|
|
|
|
1997
BORRIONE D., VESTMAN F., BOUAMAMA H.
An approach to Verilog-VHDL interoperability for synchronous designs
This paper suggests that synchronous designs written in either Verilog or
VHDL can be interpreted in terms of a common Hierarchical Finite State Machine
model, and shows the principles for extracting the semantics of designs
described in either language. Sublanguages with identical semantics are
identified, and an algorithm for inferring a minimal number of state variables
from VHDL processes is given. This common semantic model can be used as a kernel
for cycle-based simulation, formal verification, and synthesis, irrespective of
the source language. In particular, Verilog and VHDL descriptions can be proven
equivalent, and modules developed in one language can be reused in projects
documented in the other one. This approach has been prototyped by the
implementation of a semantic link between the VIS system of Berkeley and the Prevail system of TIMA.
Proc. IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods "CHARME'97", Montreal, Canada, 16-18 October, Chapman & Hall Publishers (to appear).
Postscript file.
|
WAHBA A.
Diagnostic des erreurs de conception dans les circuits digitaux: le cas des erreurs simples
Design error diagnosis in digital circuits: the case of simple errors
Automatic diagnosis of design errors is an important problem in digital
circuits CAD. Although automated synthesis tools are being used to generate
"correct-by-construction" designs, these designs are still modified manually to
perform small specification changes, or to enhance some critical design aspects.
Verification tools can discover the existence of errors, but they give no
information about their location or how to correct them, they give only
counter-examples that witness the error. What designers commonly do is simulate
their design with these counter-examples, and visually inspect the ciruit and
trace each path in it. This operation takes a very long time which may be equal
or even greater than the design time itself. In this thesis we present automated
algorithms for the location and the correction of simple design errors in logic
circuits under the single error hypothesis. The errors treated here are
component replacement errors in combinational and sequential circuits, and
connection errors in combinational circuits. The single error model implicitly
implies a "frequent verification strategy", in which the design is verified
frequently after each design change, so that the probability of inserting more
than one error is not very high. Our approach consists in simulating the circuit
under the application of a given test pattern, and then scanning it to analyse
its components. To accelerate the process we use special test patterns generated
for the diagnosis. Two prototype diagnosis tools are built based on these
algorithms. CCDS is the diagnosis tool for combinational circuits, and SCDS is
the diagnosis tool for sequential circuits. CCDS and SCDS are currently
integrated in the proof environment PREVAIL.
These de Doctorat UJF, 7 May 1997 (in French)
ftp://ftp.imag.fr/pub/Mediatheque.IMAG/theses/97-Wahba.Ayman
|
DUSHINA J., BORRIONE D.
Formalisation and validation of the Std_Logic_1164 and Numeric_Std {VHDL} packages using the Nqthm theorem prover
When synthesizing complex digital circuits, it is extremely important to have
high confidence in the library of components and functions. This paper deals
with the validation of two standardized VHDL packages that were developed for
circuit synthesis and which, at the same time, are compatible with enhanced
multi-valued simulation tools. The Boyer-Moore theorem prover has been used for
this purpose. The paper introduces an efficient and general strategy for
utilizing the basic concepts of the Boyer-Moore system to prove the theorems
that establish the mathematical properties of the package functions.
2nd Workshop on Libraries, Component Modeling and Quality Assurance, Toledo, Spain, 23-25 April 1997.
Postscript file.
|
WAHBA A., BORRIONE D.
Connection errors location and correction in combinational circuits
We present new diagnostic algorithmes for localizing connection errors in
combinational circuits. Three types of errors are considered: extra, missing,
and bad connection errors. Special test patterns are generated to rapidly locate
the error. The algorithms are integrated within the Prevail system. Results on
benchmarks show that the error is always located, within a time proportional to
the product of the circuit size, and the number of used patterns.
European Design and Test Conference ED&TC-97, Paris, France, 17-20 March 1997.
Postscript file.
|
WAHBA A.
Diagnostic des Erreurs de Composants dans les Circuits Logiques
Nous présentons dans cet article de nouveaux algorithmes pour la localisation
et la correction automatique des erreurs de composants dans les circuits
logiques. Une erreur de composant est due au remplacement d'un composant par un
autre dans une bibliothèque donnée de composants. Le diagnostic est fait à
l'aide d'un ensemble de règles et de vecteurs de test spécialement générés pour
qu'ils réduisent rapidement la zone suspecte du circuit. Un outil prototype a
été réalisé et intégré dans l'environement PREVAIL. Les tests effectués sur un
ensemble de jeux d'essai montrent l'efficacité de nos algorithmes.
Proc. Colloque CAO de circuits intégrés et systèmes: Action structurante en CAO de Circuits Intégrés et Systèmes DSPT4/MENESRIP, TIMA, pp. 102-105, Villard de Lans, Grenoble, France, 15-17 January 1997.
Postscript file
|
|
|
|
1996
DUSHINA J., BORRIONE D., JERRAYA A.
Correct reuse of complex design units during high level synthesis: verification issues
The paper proposes a new model for verification and high level synthesis (re)using
complex units like co-processors. The model is called FSMC (FSM with
Co-processors) and is an extension of the FSMD model (FSM with Data path). The
verification method is based on model checking. It permits to analyze the
properties and consistency of the whole system and, particularly, the correct (re)use of design blocks.
1st IEEE International High Level Design Validation and Test Workshop (HLDVT), Oakland, California, USA, 15-16 November 1996.
Postscript file.
|
DEHARBE D.
Vérification formelle de propriétés temporelles: étude et application au langage VHDL
Temporal logic model checking: study and application to VHDL
Model checking makes it possible to verify the behavior of a finite state
machine with respect to a temporal logic specification. Larger examples can be
verified when this technique is combined with a symbolic, BDD-based,
representation of the model states and transitions. A first barrier to the
practical use of this method remains the complexity of the model checking
algorithms. We propose a new method to represent the transitions that permits to
combine a function-based representation and a faster but more memory-consuming
transition-based representation. A second practical problem is the difficulty to
specify in the temporal logics used. We propose to add past-oriented operators
to computation tree logic CTL and give corresponding model checking algorithms.
This extension makes it simpler to express a large number of properties. The
second part of our work is the application of these methods to the verification
of VHDL descriptions. Our approach consists in, given a subset of VHDL, define a
semantics that associates a finite state machine to each description. The
verification is then carried out on these models. We first deal with a VHDL
subset similar to those accepted by commercial logic synthesis tools. The
semantics of this subset have been implemented in the verification software
SMOCK, integrated into the proof environment PREVAIL. We also present the
semantics of a larger subset and take into account the synchronization and
communication primitives of the simulation algorithm of VHDL. This work is
implemented in the program CVC.
Thèse de Doctorat UJF, 15 November 1996 (in French)
ftp://ftp.imag.fr/pub/Mediatheque.IMAG/theses/96-Deharbe.David
|
BORRIONE D., BOUAMAMA H., DEHARBE D., LE FAOU C., WAHBA A.
HDL-Based Integration of Formal Methods and CAD Tools in the PREVAIL Environment
We present an open environment for the integration of formal methods applied
to HDL descriptions of circuits. The system currently accepts SMAX and VHDL, and
provides equivalence checking, model checking, theorem proving, and automatic
diagnosis of simple design errors. After an overview of the system, we discuss
the salient features of the common intermediate format, of the diagnosis tools,
and of the automatic generation of NQTHM models from VHDL functional descriptions.
International Conference on Formal Methods in Computer-Aided Design, Palo Alto, CA, USA, 6-8 November 1996, Lectures notes in Computer Science N 1166, Springer Verlag.
Postscript file.
|
WAHBA A., BORRIONE D.
Automatic Diagnosis may Replace Simulation for Correcting Simple Design Errors
An automated tool for diagnosing simple design errors in VHDL descriptions is
presented. The tools is tested on benchmark circuits, and the results show that
the error is localized precisely, after the application of a small number of
specially generated test patterns. This tool is now integrated within the
PREVAIL system, and is being tested on industrial circuits.
Proc. European Design Automation Conference EuroDAC/EuroVHDL'96, Geneva, Switzerland, 16-20 September 1996.
Postscript file.
|
WAHBA A., BORRIONE D.
A Method for Automatic Design Error Location and Correction in Combinational Logic Circuits
We present a new diagnostic algorithm, based on backward-propagation, for
localising design errors in combinational logic circuits. Three hypotheses are
considered, that cover all single gate replacement and insertion errors.
Diagnosis-oriented test patterns are generated in order to rapidly reduce the
suspected area where the error lies. The originality of our method is the use of
patterns which do not detect the error, in addition to detecting patterns. A
theorem shows that, in favourable cases, only two patterns suffice to get a
correction. We have implemented the test generation and diagnosis algorithms.
Results obtained on benchmarks show that the error is always found, after the
application of a small number of test patterns, with an execution time
proportional to the circuit size.
Journal of Electronic Testing: Theory and Applications, Vol. 8, No. 2, pp. 113-127, Kluwer Academic Publishers, April 1996.
Postscript file.
|
BORRIONE D.
Research on VHDL in France, Italy and Switzerland
This presentation is an overview of the research on and around VHDL in
France, Italy and French speaking Switzerland. The teams covered by this survey
are well known in Europe, for their participation in the VHDL User's Groups, and
for their publications. The period covered is 1991-1995 although some groups
have started their VHDL activities several years before.
Spring VIUF Conference, Santa Clara, Californie, USA, February 1996.
|
WAHBA A., BORRIONE D.
Connection Errors Location and Correction in Combinational Circuits
We present new diagnostic routines for localizing connection errors in
combinational logic circuit designs. Special, diagnosis oriented, test patterns
are generated in order to reduce rapidly the suspected area of the circuit where
the error lies. The algorithms are implemented and the results obtained on
benchmark circuits show that the error is always found, with an execution time
proportional to the product of the circuit size, and the number of applied test patterns.
Research Report TIMA 96.1.I, INPG, Grenoble, France, February 1996.
Postscript file.
|
BORRIONE D., BOUAMAMA H., SUESCUN R.
Validation of the Numeric_Bit package using the NQTHM theorem prover
The validation of a VHDL package of parameterized functions requires general
purpose theorem proving techniques. It must be based on the formalization of the
VHDL primitives, in logic. This paper presents a general approach, using the
Boyer-Moore theorem prover, and its application to a synthesis package being
standardized. The impact of the formal validation on the package development is discussed.
Proc. APCHDL'96 Conference, Bengalore, India, January 1996.
|
BORRIONE D., LE FAOU C.
Technical Report - JESSI AC3 Project
This report describes functional verification of models with the existing formal proof techniques and tools. The different parts are:
- proof of repetitive circuits
- proof of properties
- automatic diagnosis of design errors
- validation of arithmetic VHDL packages for synthesis.
Final report - JESSI AC3 - HDL, Component Modelling and Libraries, Grenoble, France, January 1996.
|
|
|
|
1995
BAYOL C.
Une Approche Structurelle et Comportementale de Modélisation pour la Vérification de Composants VLSI
A Structural and Behavioral Modeling Approach for the Verification of VLSI Components
The manuscript describes a modeling and validation methodology for the design
of microprogrammed circuits that implement network communication protocols. The
method was developped in the framework of the FICOMP project, wich implements
the FIELDBUS protocol standard. The first chapter describes the industrial
context of the project, the various specification levels for the circuit and the
simulation and verification tools at hand. Chapter two presents the VOVHDL
language, an extension of VHDL for the specification of communications and
synchronisations among concurrent processes; a synchronous semantics in terms of
labeled transition systems is given for VOVHDL. Chapter three presents a
modeling approach for hierarchical VOVHDL descriptions, and shows its
application to the FICOMP circuit: internal modules are interconnected with a
communication module to build a highter level module; this model is then
translated into the input format of the ASA+ verification software. Chapter four
recalls the essential features of VHDL, and formalize its simulation semantics
in terms of labeled transition systems. The application of the methodology to
the specification of two modules of the FICOMP circuit, and their translation
into the proposed model, are detailed in the appendices.
Doctorat de l'Université Joseph FOURIER - Grenoble 1, 12 décembre 1995.
ftp://ftp.imag.fr/pub/Mediatheque.IMAG/theses/95-Bayol.Catherine
|
BORRIONE D., EVEKING H.*
Formal verification of hardware designs
This tutorial paper presents the principles of several complementary methods
for the automatic formal verification of digital circuits designs described in a
conventional hardware description language. VHDL is used throughout this paper,
but the methods are general. Two types of correctness are considered:
input/output equivalence between a specification and an implementation, and
verification of temporal properties. We review the representation and
manipulation of boolean functions by ordered binary decision diagrams. We show
how this technique can efficiently be used to construct equivalence checkers for
zero-delay combinational circuits and clock synchronized sequential circuits, as
well as symbolic model checkers. The verification of parameterized library
modules requires general purpose deduction mechanisms. We introduce the
application of the Boyer-Moore theorem prover for the validation of a synthesis
package. We end on the integration of the various proof systems in a single
formal verification environment.
Journal of the Brazilian Computer Society, Special Issue on Electronic
Design Automation, November 1995.
*Technische Hochschule Darmstadt, Germany.
|
WAHBA A., BORRIONE D.
Design Error Diagnosis in Sequential Circuits
We present a new diagnostic algorithm for localising design errors in
sequential circuits. The specification and the implementation may have different
number of state variables and different state encoding. The algorithm is based
on the new concept of possible next states describing the possible states of the
circuit due to the existence of the error. Results obtained on benchmark
circuits show that the error is always found, with an execution time
proportional to the product of the circuitsize, and the length of the test
sequence used.
Correct Hardware Design and Verification Methods, IFIP WG 10.5 Advanced
Research Working Conference, CHARME '95, Frankfurt/M., Germany, Lecture Notes in
Computer Science N 987, Springer Verlag, 2-4 October 1995.
Postscript file.
|
DEHARBE D., BORRIONE D.
Semantics of a Verification-Oriented subset of VHDL
This paper gives operational semantics for a subset of VHDL in terms of
abstract machines. Restrictions to the VHDL source code are the finiteness of
data types and the absence of quantitative timing informations. The abstract
machine of a design unit is built by composition of the abstract machines for
its embedded processes and blocks. The kernel process in our model is
distributed among the composed machines. One transition of the final abstract
machine models a VHDL delta cycle. This model can be used for symbolic model
@checking and equivalence verification.
Correct Hardware Design and Verification Methods, IFIP WG 10.5 Advanced
Research Working Conference, CHARME '95, Frankfurt/M., Germany, Lecture Notes in
Computer Science N 987, Springer Verlag, 2-4 October 1995.
|
BORRIONE D., SALEM A.
Denotational semantics of a synchronous VHDL subset
A denotational definition for a single clock synchronous subset of VHDL is
proposed. The different domains for variables and signals, the elaboration of
static environments, and the formulation of a simulation algorithm for the
sub-language characterize this definition, and distinguish it from more
traditional denotational semantics of programming languages.
Formal Methods in System Design, Vol 7, Ndeg. 1-2, August 1995.
|
WAHBA A.
General Survey on Sequential Test Generation Methods
In this report we survey the research that has been done in the area of test pattern generation for sequential circuits. Test pattern generation was originally made for stuck-at fault model. At the end of this report we show the relation between the stuck-at fault model and the other models. We conclude by showing how we can use the same test generation techniques under different error models.
Research Report RR-948-I, ARTEMIS-IMAG, Grenoble, France, July 1995.
Postscript file.
|
DEHARBE D., BORRIONE D.
Symbolic model checking with past and future temporal modalities: fundamentals and algorithms current issues in electronic modeling
Volume 1 on Model Generation in Electronic Design, Kluwer, march 1995.
|
|
|
Current Members 
