Formal Verification Method for Combinatorial Circuits at High Level Design

	This Article
	Subscribers, please Login Purchase article: $19 PDF IEEE Xplore Subscribers RSS feed
	Share
	Email this Article to a friend
	Bibliographic References
	ASCII Text BibTex RefWorks Procite/RefMan/Endnote
	Add to:
	Digg Furl Spurl Blink Simpy Google Del.icio.us Y!MyWeb
	Search
	Similar Articles Articles by Junji Kitamichi Articles by Hiroyuki Kageyama Articles by Nobuo Funabiki

Asia and South Pacific Design Automation Conference 1999 (ASP-DAC'99)

Wanchai, Hong Kong

January 18-January 21

ISBN: 0-7803-5012-X

	ASCII Text	x
	Junji Kitamichi, Hiroyuki Kageyama, Nobuo Funabiki, "Formal Verification Method for Combinatorial Circuits at High Level Design," Asia and South Pacific Design Automation Conference, pp. 319, Asia and South Pacific Design Automation Conference 1999 (ASP-DAC'99), 1999.

	BibTex	x
	@article{ 10.1109/ASPDAC.1999.760023, author = {Junji Kitamichi and Hiroyuki Kageyama and Nobuo Funabiki}, title = {Formal Verification Method for Combinatorial Circuits at High Level Design}, journal ={Asia and South Pacific Design Automation Conference}, volume = {0}, year = {1999}, isbn = {0-7803-5012-X}, pages = {319}, doi = {http://doi.ieeecomputersociety.org/10.1109/ASPDAC.1999.760023}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }

	RefWorks Procite/RefMan/Endnote	x
	TY - CONF JO - Asia and South Pacific Design Automation Conference TI - Formal Verification Method for Combinatorial Circuits at High Level Design SN - 0-7803-5012-X SP EP A1 - Junji Kitamichi, A1 - Hiroyuki Kageyama, A1 - Nobuo Funabiki, PY - 1999 KW - null VL - 0 JA - Asia and South Pacific Design Automation Conference ER -

Junji Kitamichi, Osaka University, Japan

Hiroyuki Kageyama, Osaka University, Japan

Nobuo Funabiki, Osaka University, Japan

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/ASPDAC.1999.760023

In this paper, we propose a formal verification method for combinatorial circuits at high level design. The specification is described by both integer and Boolean variables for input and output variables, and the implementation is described by only Boolean variables. Our verification method judges the equivalence between the specification and the implementation by deciding the truth of Presburger sentence. We show experimental results on some benchmarks, such as 4bit ALU, multiplier, by our method.

Citation:

Junji Kitamichi, Hiroyuki Kageyama, Nobuo Funabiki, "Formal Verification Method for Combinatorial Circuits at High Level Design," asp-dac, pp.319, Asia and South Pacific Design Automation Conference 1999 (ASP-DAC'99), 1999

Peer Review Notice | Give Us Feedback

Usage of this product signifies your acceptance of the Terms of Use.