Integrating Formal Verification into an Advanced Computer Architecture Course  

Oleh:

Velvev, Miroslav N.

Jenis: Article from Journal - ilmiah internasional
Dalam koleksi: IEEE Transactions on Education vol. 48 no. 2 (May 2005), page 216-222.
Topik: Abstraction; Boolean Stability (SAT); Computer Architecture; Formal Verification of Microprocessors Design; Logic of Equality with Uninterpreted Functions and Memories (EUFM); Positive Equality Teacghing of Formal Methods

Ketersediaan

Perpustakaan Pusat (Semanggi) Nomor Panggil: II71.1 Non-tandon: 1 (dapat dipinjam: 0) Tandon: tidak ada

Lihat Detail Induk

Isi artikel

This paper presents a sequence of three projects on design and formal verification of pipelined and superscalar processors: 1) a single-issue, five-stage DLX (an academic processor used widely for teaching pipelined execution and defined by Hennessy and Patterson in the first edition of their graduate textbook); 2) an extension of the DLX with exceptions and branch prediction; and 3) a dual-issue superscalar DLX. The projects were integrated into two editions of an advanced computer architecture course that was offered at the Georgia Institute of Technology, Atlanta, in the summer and fall 2002 and was taught to 67 students (25 of whom were undergraduates) in a way that required them to have no prior knowledge of formal methods. Preparatory homework problems included an exercise on design and formal verification of a staggered Arithmetic Logic Unit (ALU), pipelined in the style of the integer ALUs in the Intel Pentium 4. The processors were designed and formally verified with a tool flow that was used to formally verify the M/spl middot/CORE processor at Motorola and detected bugs.

Opini Anda

Klik untuk menuliskan opini Anda tentang koleksi ini!

Kembali