|
Accession number;99A0263648
|
| Title;Formal Verification of Hardware Described in HDL Using Temporal Logic. |
| Author;
ARARAGI TADASHI
(Nippon Telegr. and Teleph. Corp.)
SAWADA HIROSHI
(Nippon Telegr. and Teleph. Corp.)
|
Journal Title;IEIC Technical Report (Institute of Electronics, Information and Communication Engineers)
|
Journal Code:S0532B
|
ISSN:0913-5685
|
|
VOL.98;NO.498(AI98 62-67);PAGE.33-40(1999)
|
| Figure&Table&Reference;FIG.4, REF.4 |
| Pub. Country;Japan |
| Language;Japanese |
| Abstract;In this paper, we introduce a method of formally verifying specifications on hardware directly from their descriptions in HDL(Hardware Description Language). The method is focused on SFL, the HDL of the hardware synthesis system PARTHENON. The essential part of the method is transformation of SFL descriptions to the Boolean formulas which represent the relation of state transition of the hardware. In this transformation, several devices are required to create the Boolean formula that behaves precisely in accordance with the semantics of SFL when it is applied to the standard backward model checking algorithm of temporal logic CTL. We discuss the problem in detail. (author abst.) |
|
|
|
Related Articles;
|
