Presentation 1995/10/19
Efficient Construction of Binary Moment Diagrams for Verifying Arithmetic Circuits
Kiyoharu HAMAGUCHI, Akihito MORITA, Shuzo YAJIMA,
PDF Download Page PDF download Page Link
Abstract(in Japanese) (See Japanese page)
Abstract(in English) BDD-based approaches cannot handle some arithmetic functions such as multiplication efficiently, while Binary Moment Diagrams proposed by Bryant and Chen provide compact representations for those functions. They reported a BMD-based polynomial-time algorithm for verifying multipliers. This approach requires high-level information such as specifications to subcomponents. This paper presents a new technique called backward construction which can construct BMDs directly from circuit descriptions without any high-level information. We have successfully verified 64-bit multipliers of several type. This result outperforms previous BDD-based approaches for verifying multipliers.
Keyword(in Japanese) (See Japanese page)
Keyword(in English) formal verification / equivalence checking / binary moment diagram / arithmetic circuit
Paper # VLD95-84,FTS95-46
Date of Issue

Conference Information
Committee VLD
Conference Date 1995/10/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 VLSI Design Technologies (VLD)
Language ENG
Title (in Japanese) (See Japanese page)
Sub Title (in Japanese) (See Japanese page)
Title (in English) Efficient Construction of Binary Moment Diagrams for Verifying Arithmetic Circuits
Sub Title (in English)
Keyword(1) formal verification
Keyword(2) equivalence checking
Keyword(3) binary moment diagram
Keyword(4) arithmetic circuit
1st Author's Name Kiyoharu HAMAGUCHI
1st Author's Affiliation Dept. of Information Science, Kyoto University()
2nd Author's Name Akihito MORITA
2nd Author's Affiliation Tokyo Marine and Fire Insurance Co., Ltd.
3rd Author's Name Shuzo YAJIMA
3rd Author's Affiliation Dept. of Information Science, Kyoto University
Date 1995/10/19
Paper # VLD95-84,FTS95-46
Volume (vol) vol.95
Number (no) 306
Page pp.pp.-
#Pages 8
Date of Issue