Formal verification of pipelined and superscalar processors

Author

Shonai, Tom ; Shimizu, Tsuguo

Author_Institution

Central Res. Lab., Hitachi Ltd., Tokyo, Japan

fYear

1995

fDate

29 Aug-1 Sep 1995

Firstpage

513

Lastpage

518

Abstract

We describe a formal verification algorithm for pipelined and superscalar processors. This algorithm proves the equivalence between a processor´s design and its specifications by rewriting recursive functions and using a new type of mathematical induction: extended recursive induction. Partial unfolding makes it possible to derive superscalar specifications from instruction-wise specifications. After the user indicates only selectors in the design, this algorithm can automatically prove correctness. The performance is independent of not only data width but also memory size. Experimental results are also presented

Keywords

formal verification; logic CAD; logic design; logic testing; pipeline processing; recursive functions; extended recursive induction; formal verification; mathematical induction; pipelined processors; recursive functions; rewriting; superscalar processors; superscalar specifications; unfolding; Algorithm design and analysis; Automata; Central Processing Unit; Formal verification; Humans; Laboratories; Logic circuits; Pipelines; Process design; Timing;

fLanguage

English

Publisher

ieee

Conference_Titel

Design Automation Conference, 1995. Proceedings of the ASP-DAC '95/CHDL '95/VLSI '95., IFIP International Conference on Hardware Description Languages. IFIP International Conference on Very Large Scal

Conference_Location

Chiba

Print_ISBN

4-930813-67-0

Type

conf

DOI

10.1109/ASPDAC.1995.486363

Filename

486363