Toru SHONAI

Invariant-Free Formal Verification of Pipelined and Superscalar Controls by Behavior-Covering and Partial Unfolding
Toru SHONAI Tsuguo SHIMIZU 
Publication:   IEICE TRANSACTIONS on Information and Systems
Publication Date: 1999/02/25
Vol. E82-D  No. 2  pp. 376-388
Type of Manuscript:  PAPER
Category: Computer Hardware and Design
Keyword: 
formal verification, processor, pipeline, superscalar, 
 Summary | Full Text:PDF
Proposal for Incremental Formal Verification
Toru SHONAI Kazuhiko MATSUMOTO 
Publication:   IEICE TRANSACTIONS on Information and Systems
Publication Date: 1998/11/25
Vol. E81-D  No. 11  pp. 1172-1185
Type of Manuscript:  PAPER
Category: Computer Hardware and Design
Keyword: 
formal verification, processor, pipeline, BDD, theorem prover, 
 Summary | Full Text:PDF
Formal Verification System for Pipelined Processors
Toru SHONAI Tsuguo SHIMIZU 
Publication:   IEICE TRANSACTIONS on Fundamentals of Electronics, Communications and Computer Sciences
Publication Date: 1996/06/25
Vol. E79-A  No. 6  pp. 883-891
Type of Manuscript:  PAPER
Category: VLSI Design Technology and CAD
Keyword: 
formal verification, pipeline, processor, correctness, mathematical induction, 
 Summary | Full Text:PDF
A Formal Verification Algorithm for Pipelined Processors
Toru SHONAI Tsuguo SHIMIZU 
Publication:   IEICE TRANSACTIONS on Fundamentals of Electronics, Communications and Computer Sciences
Publication Date: 1995/05/25
Vol. E78-A  No. 5  pp. 618-631
Type of Manuscript:  PAPER
Category: VLSI Design Technology and CAD
Keyword: 
formal verification, hardware verification, specifications, design correctness, proof, pipeline invariant, 
 Summary | Full Text:PDF