SMU CSE 5381/7381 "Computer Architecture" Fall 2003

Research Directions

Overview & References

Dr. Peter-Michael Seidel

General Links

CSE Colloquium Series
CSE Distinguished Lecture Series
Degree Programs in Computer Science and Engineering @ SMU
Application Forms for Graduate Students
Advice for Graduate Students
Computing Research Association (CRA)
The Collection of Computer Science Bibliographies
Scientific Literature Digital Library (CITESEER)
U.S. Patent Database Page
Conferences Calendar by IEEE & ACM
Turing Awards & Turing Award Lectures

Topics

Formal Verification

Project Abstracts

Summary: Formal Arithmetic Circuit Verification Research (FAVoR).

Summary: Formal Verification for Practical Design Flows.

Theorem Proving Environments

PVS homepage (PVS Tutorials)
Isabelle/HOL homepage (Tutorial)

Kroening, D., Formal Verification of Pipelined Microprocessors, PhD Thesis, University of the Saarland, 2001.
Jacobi, C., Formal Verification of a Fully IEEE Compliant Floating Point Unit, PhD Thesis, University of the Saarland, 2002.
Berg, C., Formal verification of an IEEE floating point adder. Master's thesis, University of the Saarland, May 2001. (pvs-files).
Seidel, P.-M., On the Design and Quantitative Analysis of IEEE Compliant Floatin-Point Units (with correctness proofs), PhD thesis, University of the Saarland, 1999.

Berg, C., Beyer, S., Jacobi, C., Kröning, D., and Leinenbach, D., Formal verification of the VAMP microprocessor (project status). In Proc. Symp. on the Effectiveness of Logic in Computer Science (ELICS02), MPI-I-2002-2-007, pages 31-36, March 2002. (slides) (poster).
Berg, C. and Jacobi, C., Formal verification of the VAMP floating point unit. In CHARME 2001, LNCS 2144, pages 325-339. Springer, Sept. 2001. (slides)
Berg, C., Jacobi, C., and Kroening, D., Formal verification of a basic circuits library. In Applied Informatics 2001, pages 252-255. ACTA Press, February 2001. (slides)

Others

Paul, W.J.. Lecture notes on Formal Computer Architecture I, University of the Saarland, compiled by students in Fall 2001.
Mueller, S.M., Paul, W.J., Computer Architecture - Complexity & Correctness, ISBN 3-540-67481-0, Springer Verlag, 2000.
--> Errata.

References Microprocessor Verification

Algebraic Models of Correctness for Microprocessors

A.C.J. Fox and N.A. Harman, Algebraic Models of Correctness for Microprocessors. Formal Aspects of Computing, 12(4): 298-312, 2000.
A.C.J. Fox An Algebraic Models for Advanced Microprocessors., PhD thesis, University of Wales Swansea, 1998.

Specification and Verification of Microprocessors in HOL

A.C.J. Fox An Algebraic Framework for Modelling and Verifying Microprocessors Using HOL., 2001.
A.C.J. Fox, A HOL Specification of the ARM Instruction Set Architecture. Technical report No. 545, University of Cambridge Computer Laboratory, June 2001.
A.C.J. Fox, Formal verification of the ARM6 micro-architecture. Technical report No. 548, University of Cambridge Computer Laboratory, November 2002.

Automatic Generation of Invariants in Processor Verification

Jeffrey X. Su, David L. Dill, Clark W. Barrett, Automatic Generation of Invariants in Processor Verification. First international conference on formal methods in computer-aided design 1996.
Z. Manna, A. Pnueli Temporal Verification of Reactive Systems, Safety. Springer-Verlag, 1995 (p.104-152).

Top-level Refinement in Processor Verification

S.Krstic, B.Cook, J.Launchbury, J.Matthews, "Top-level Refinement in Processor Verification", 1998
J.Burch, D.Dill , "Automatic verification of pipelined microprocessor control", 1994.

Verification of Out-Of-Order Processor Designs Using Model Checking and a Light-Weight Completion Function

S. Berezin, E. Clarke, A. Biere, Y. Zhu, "Verification of Out-Of-Order Processor Designs Using Model Checking and a Light-Weight Completion Function", 2002
S. Berezin, A. Biere, E. Clarke, andY. Zhu, Combining symbolic model checking with uninterpreted functions for out-of-order processor verification, 1998.

Specification and Verification of HDL models (2 themes)

David M. Russinoff, Specification and Verification of Gate-Level VHDL Models of Synchronous and Asynchronous Circuits. 1994.

Hardware Verification using Monadic Second Order Logic

David A. Basin, Nils Klarrund, Hardware Verification using Monadic Second Order Logic. 1995
A. Aziz, F.Balarin, K.Brayton, A.Sangiovanni-Vincentelli "Sequential Synthesis Using SIS", 2000.

Verification of Synchronous Circuits by Symbolic Logic Simulation

R.E.Bryant, "Verification of Synchronous Circuits by Symbolic Logic Simulation", 1989.

Relative Timing Based Verification of Timed Circuits and Systems

H.Kim, P.A.Beerel, K.Stevens "Relative Timing Based Verification of Timed Circuits and Systems", 2001.

Formal Specification of Abstract Memory Models (Proseminar)

David L. Dill and Seungjoon Park and Andreas G. Nowatzyk, "Formal Specification of Abstract Memory Models," Proceedings of the 1993 Symposium, Gaetano Borriello and Carl Ebeling, Eds. MIT Press, 1993, pp 38-52.

Verification of Operating Systems
...

Verification of Compilers
...

Software Verification

Peled, D., Software Reliability Methods, Springer 2001.
Manna, Z. and Pnueli, A., Temporal Verification of Reactive Systems, Springer 1995.

Model Checking

Temporal Logic (summary report: Anton Myagotin )

Clarke, Grumberg, Peled - Model Checking (1999): chapters 2, 3

Emerson - Temporal and Modal Logic (1990), in: van Leuwwen - Handbook of Theoretical Computer Science (Vol. B)

Model Checking Algorithms (summary report: Igor Glinyanitsa

)

Clarke, Emerson, Sistla - Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications (Journal Version, 1986)

Lichtenstein, Pnueli - Checking That Finite State Concurrent Programs Satisfy Their Linear Specifications (1985)

Symbolic Model Checking (summary report: Sergey Tverdyshev

)

Burch, Clarke, McMillan - Symbolic Model Checking: 1020 States and Beyond (Journal Version, 1992)

Compositional Reasoning (summary report: Ewgenij Filonenko )

Clarke, Long, McMillan - Compositional Model Checking (1989)

Grumberg, Long - Model Checking and Modular Verification (1991).

Symmetry (summary report: Elena Petrova )

Ip, Dill - Better Verification Through Symmetry (1993)

Ip, Dill - Better Verification Through Symmetry (Journal Version, 1996)

Emerson, Sistla - Symmetry and Model Checking (1994).

Abstraction (summary report: Ramesh Kumar )

Clarke, Grumberg, Long - Model Checking and Abstraction (1999)

Equivalence Checking
...

Computer Arithmetic

Building the arith.org homepage

Current Graduate Course on Computer Arithmetic

Current Research Projects in CSE8351:

Radix-k Serial FP-Adder
Formal Verification of optimized Arithmetic Hardware
Scalable multiplicative FP-Dividers
Effective Binary Multiplication on FPGAs
Evaluating Very-High-Radix Division on FPGAs
Multiple-Path Fused Multiply-Add
Shift-less Floating-Point Addition
Low-Precision Arithmetic for Computer Graphic Algorithms
Application-Specific Arithmetic for Speech Processing

Bibliography on Computer Arithmetic

Bibliography of Material on Floating-Point Arithmetic

References for Floating-Point on FPGAs

Belanovic et al, A Library of Parameterized Floating-Point Modules and Their Use. FPL 2002.

Liang, Tessier et al, Floating Point Unit Generation and Evaluation for FPGAs, FCCM 2003.

Lee & Burgess, Parameterisable Floating-point Operations on FPGA, Asilomar 2002.

http://www.fpgacpu.org/usenet/fp.html

Ligon et al, A Re-evaluation of the practicality of floating-point operations on FPGAs, FCCM 1998

Lourca et al, Implementation of IEEE single precision floating point addition and multiplication on FPGAs, FCCM 1996

Shirazi et al, Quantitative analysis of floating point arithmetic on FPGA based custom computing machines, FCCM 1995

Leong et al, Automating floating to fixed point translation and its application to post-rendering 3D warping, FCCM 1999

Fagin, B. and Renard, C., Field Programmable Gate Arrays and Floating-Point Arithmetic, IEEE

Transactions on VLSI Systems, vol. 2, No. 3, Sept. 1994.

Fagin & Renard, Field Programmable Gate Arrays and Floating-Point Arithmetic, ???, the same as above?.

Effective & Adaptive Parallelism

Project Abstracts

Summary: Effective and Adaptive Parallelism.

Summary: PRAM-on-a-Chip

Effective & Adaptive Parallelism

Fundamental and Technical aspects of Effectivity in Digital Systems

Current Projects in CSE5381 & CSE7381
Undergraduate Projects:

Functional Traces for PISA, MIPS and Alpha and Comparison between each other and with running hardware (Alpha and MIPS), bit width analysis and de-normalized operand extraction (2P)
Determining Instruction set (and encoding) for minimum bit width that is compatible to MIPS and implementation in hardware and software. (2P)
Quantitative Evaluation and Comparison of Commercial Memory protocols and chipsets. (2P)
Survey on graphic hardware architectures and summary of quantitative properties (1P)

Graduate Projects:

IEEE FP Software/Hardware Co-Design (3P)
Implement optimized FP routines (with and w/o FP register support)
Measure FP trap routine lengths from existing implementations (various Architectures)
Measure lengths of FP software routines from compiled code for target architectures w/o FP hardware support.
Quantitatively evaluate and compare with FP hardware solutions
Implementation of Scalable Super Pipeline with forwarding and stalling (3P)
Parametric Implementation, Quantitative Evaluation of Cost and Delay
Determine optimal pipeline depth in dependency of q
Power analysis of pipelined Implementation (3P)
Statistics for switching activity for each pipeline stage, Power estimation for each
pipeline stage. Determine Power dependencies on instructions and benchmarks.
Scaling of Bit width (fixed point) in pipelined/superscalar Implementation (3P)
Parametric Implementation, Quantitatively evaluate cost/delay, Determine optimal
bit width in dependency of q
Out-of Order and Pipelined Cache Design and Evaluation (3P)
Implement out-of-order memory hierarchies, Determine Hardware overhead
Evaluate speedup depending on memory protocol parameters.
Compressed instruction memory (MIPS) (3P)
Discussion of compression and organization , Implementation for pipelined design
Evaluation of Speedup depending on memory protocol parameters.
Redundant format datapaths in pipelined/superscalar implementation (2-3P)
Implementation of redundant datapaths, Evaluation of cost and cycle times
Performance evaluation and comparison for benchmark applications considering
realistic memory parameters