Paper Abstract and Keywords |
Presentation |
2014-11-26 10:45
A hardware description method and sematics providing a timing constrant Shunji Nishimura, Motoki Amagasaki, Toshinori Sueyoshi (Kumamoto Univ.) VLD2014-82 DC2014-36 |
Abstract |
(in Japanese) |
(See Japanese page) |
(in English) |
Formal verification methods are wide-spreading due to its mathmatical rigorousaspect, although they limited to synchrounous circiut.For an asynchronou circuit, It is almost no meaning in verification along undefined delayvalues on circuit description phase.In this article, we propose a hardware description method and semantics providing a timingconstraint to allow verification of an asynchronous circuit.The description method is component-centered by introducing a concept ofArrows 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 descriptionmethod and semantics.We also show an implementation of the description and semantics on theorem prover Agda. |
Keyword |
(in Japanese) |
(See Japanese page) |
(in English) |
hardware description / timing constraint / formal method / formal verification / asynchronous circuit / / / |
Reference Info. |
IEICE Tech. Rep., vol. 114, no. 328, VLD2014-82, pp. 81-86, Nov. 2014. |
Paper # |
VLD2014-82 |
Date of Issue |
2014-11-19 (VLD, DC) |
ISSN |
Print edition: ISSN 0913-5685 Online edition: ISSN 2432-6380 |
Copyright and reproduction |
All rights are reserved and no part of this publication may be reproduced or transmitted in any form or by any means, electronic or mechanical, including photocopy, recording, or any information storage and retrieval system, without permission in writing from the publisher. Notwithstanding, instructors are permitted to photocopy isolated articles for noncommercial classroom use without fee. (License No.: 10GA0019/12GB0052/13GB0056/17GB0034/18GB0034) |
Download PDF |
VLD2014-82 DC2014-36 |
Conference Information |
Committee |
VLD DC IPSJ-SLDM CPSY RECONF ICD CPM |
Conference Date |
2014-11-26 - 2014-11-28 |
Place (in Japanese) |
(See Japanese page) |
Place (in English) |
B-ConPlaza |
Topics (in Japanese) |
(See Japanese page) |
Topics (in English) |
Design Gaia 2014 -New Field of VLSI Design- |
Paper Information |
Registration To |
VLD |
Conference Code |
2014-11-VLD-DC-SLDM-CPSY-RECONF-ICD-CPM |
Language |
Japanese |
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 |
Keyword(6) |
|
Keyword(7) |
|
Keyword(8) |
|
1st Author's Name |
Shunji Nishimura |
1st Author's Affiliation |
Kumamoto University (Kumamoto Univ.) |
2nd Author's Name |
Motoki Amagasaki |
2nd Author's Affiliation |
Kumamoto University (Kumamoto Univ.) |
3rd Author's Name |
Toshinori Sueyoshi |
3rd Author's Affiliation |
Kumamoto University (Kumamoto Univ.) |
4th Author's Name |
|
4th Author's Affiliation |
() |
5th Author's Name |
|
5th Author's Affiliation |
() |
6th Author's Name |
|
6th Author's Affiliation |
() |
7th Author's Name |
|
7th Author's Affiliation |
() |
8th Author's Name |
|
8th Author's Affiliation |
() |
9th Author's Name |
|
9th Author's Affiliation |
() |
10th Author's Name |
|
10th Author's Affiliation |
() |
11th Author's Name |
|
11th Author's Affiliation |
() |
12th Author's Name |
|
12th Author's Affiliation |
() |
13th Author's Name |
|
13th Author's Affiliation |
() |
14th Author's Name |
|
14th Author's Affiliation |
() |
15th Author's Name |
|
15th Author's Affiliation |
() |
16th Author's Name |
|
16th Author's Affiliation |
() |
17th Author's Name |
|
17th Author's Affiliation |
() |
18th Author's Name |
|
18th Author's Affiliation |
() |
19th Author's Name |
|
19th Author's Affiliation |
() |
20th Author's Name |
|
20th Author's Affiliation |
() |
Speaker |
Author-1 |
Date Time |
2014-11-26 10:45:00 |
Presentation Time |
25 minutes |
Registration for |
VLD |
Paper # |
VLD2014-82, DC2014-36 |
Volume (vol) |
vol.114 |
Number (no) |
no.328(VLD), no.329(DC) |
Page |
pp.81-86 |
#Pages |
6 |
Date of Issue |
2014-11-19 (VLD, DC) |
|