Universität des Saarlandes
Fachbereich Informatik
Compiler Design Lab
Bau 45, Raum 404
66123 Saarbrücken, Germany
cb(at)cs.uni-sb.de
http://rw4.cs.uni-sb.de/~cb/
Phone: +49 (681) 302-5573
Fax: +49 (681) 302-3065
| [BBJ+02] |
Christoph Berg, Sven Beyer, Christian Jacobi, Daniel Kröning, and Dirk
Leinenbach.
Formal verification of the VAMP microprocessor (project status).
In Witold Charatonik and Harald Ganzinger, editors, Symposium on
the Effectiveness of Logic in Computer Science (ELICS02), number
MPI-I-2002-2-007, pages 31-36. Max-Planck-Institut für Informatik, March
2002. [ bib | poster | slides | .ps.gz ] |
| [BJ01] |
Christoph Berg and Christian Jacobi.
Formal verification of the VAMP floating point unit.
In CHARME 2001, volume 2144 of LNCS, pages 325-339.
Springer, September 2001. [ bib | slides | .pdf ]
We report on the formal verification of the floating point unit used in the VAMP processor. The FPU is fully IEEE compliant, and supports denormals and exceptions in hardware. The supported operations are addition, subtraction, multiplication, division, comparison, and conversions. The hardware is verified on the gate level against a formal description of the IEEE standard by means of the theorem prover PVS.
|
| [Ber01] |
Christoph Berg.
Formal verification of an IEEE floating point adder.
Master's thesis, Saarland University, Computer Science Department,
May 2001. [ bib | PVS files | .ps.gz | .ps | .pdf ]
Our group at Saarland University is formally verifying the correctness of a complete microprocessor called VAMP. The PVS theorem prover is used to specify the circuit definitions and to prove their correctness. For the VAMP project, a library of basic circuits was developed. The formal verification of this library is described in the first part of this thesis. Part of the VAMP is an IEEE compliant floating point unit. The second part of this thesis describes the formal verification of the gate level correctness of the VAMP floating point adder.
|
| [BJK01] |
Christoph Berg, Christian Jacobi, and Daniel Kroening.
Formal verification of a basic circuits library.
In Applied Informatics 2001, pages 252-255. ACTA Press,
February 2001. [ bib | slides | .ps.gz | .ps | .pdf ]
We describe the results and status of a project aiming to provide a provably correct library of basic circuits. We use the theorem proving system PVS in order to prove circuits such as incrementers, adders, arithmetic units, multipliers, leading zero counters, shifters, and decoders. All specifications and proofs are available on the web.
|
| [Ber99] |
Christoph Berg.
Flachbandkabel-Tester für das SB-PRAM-Projekt.
Saarland University, Computer Science Department, October 1999.
(In German). [ bib | .ps.gz ] |
| Christoph Berg <cb(at)cs.uni-sb.de> | Page last changed on Fri Mar 14 17:26 2003 |