Presentation | 2014-11-26 A hardware description method and sematics providing a timing constrant Shunji NISHIMURA, Motoki AMAGASAKI, Toshinori SUEYOSHI, |
---|---|
PDF Download Page | PDF download Page Link |
Abstract(in Japanese) | (See Japanese page) |
Abstract(in English) | Formal verification methods are wide-spreading due to its mathmatical rigorous aspect, although they limited to synchrounous circiut. For an asynchronou circuit, It is almost no meaning in verification along undefined delay values on circuit description phase. In this article, we propose a hardware description method and semantics providing a timing constraint to allow verification of an asynchronous circuit. The description method is component-centered by introducing a concept of Arrows that is a class of a programming language. The semantics employs an abstract delay under Kripke semantics of modal logic. Verification of an asynchronous circuit become possible with applying the description method and semantics. We also show an implementation of the description and semantics on theorem prover Agda. |
Keyword(in Japanese) | (See Japanese page) |
Keyword(in English) | hardware description / timing constraint / formal method / formal verification / asynchronous circuit |
Paper # | VLD2014-82,DC2014-36 |
Date of Issue |
Conference Information | |
Committee | DC |
---|---|
Conference Date | 2014/11/19(1days) |
Place (in Japanese) | (See Japanese page) |
Place (in English) | |
Topics (in Japanese) | (See Japanese page) |
Topics (in English) | |
Chair | |
Vice Chair | |
Secretary | |
Assistant |
Paper Information | |
Registration To | Dependable Computing (DC) |
---|---|
Language | JPN |
Title (in Japanese) | (See Japanese page) |
Sub Title (in Japanese) | (See Japanese page) |
Title (in English) | A hardware description method and sematics providing a timing constrant |
Sub Title (in English) | |
Keyword(1) | hardware description |
Keyword(2) | timing constraint |
Keyword(3) | formal method |
Keyword(4) | formal verification |
Keyword(5) | asynchronous circuit |
1st Author's Name | Shunji NISHIMURA |
1st Author's Affiliation | Graduate School of Science and Technology, Kumamoto University() |
2nd Author's Name | Motoki AMAGASAKI |
2nd Author's Affiliation | Graduate School of Science and Technology, Kumamoto University |
3rd Author's Name | Toshinori SUEYOSHI |
3rd Author's Affiliation | Graduate School of Science and Technology, Kumamoto University |
Date | 2014-11-26 |
Paper # | VLD2014-82,DC2014-36 |
Volume (vol) | vol.114 |
Number (no) | 329 |
Page | pp.pp.- |
#Pages | 6 |
Date of Issue |