IEICE Trans

Kiyoharu HAMAGUCHI

FOREWORD Kiyoharu HAMAGUCHI
Publication: Publication Date: 2019/07/01 Vol. E102-A No. 7 pp. 866-866 Type of Manuscript: FOREWORD Category: Keyword:
	Summary \| Full Text:PDF

FOREWORD Kiyoharu HAMAGUCHI
Publication: Publication Date: 2018/12/01 Vol. E101-A No. 12 pp. 2221-2221 Type of Manuscript: FOREWORD Category: Keyword:
	Summary \| Full Text:PDF

Applying an SMT Solver to Coverage-Driven Design Verification Kiyoharu HAMAGUCHI
Publication: Publication Date: 2018/07/01 Vol. E101-A No. 7 pp. 1053-1056 Type of Manuscript: Special Section LETTER (Special Section on Design Methodologies for System on a Chip) Category: Keyword: RTL verification, coverage-driven verification, SAT solver, SMT solver, automated testbench,
	Summary \| Full Text:PDF

Coverage-Driven Design Verification Using a Diverse SAT Solver Yosuke KAKIUCHI Kiyoharu HAMAGUCHI
Publication: Publication Date: 2017/07/01 Vol. E100-A No. 7 pp. 1481-1487 Type of Manuscript: Special Section PAPER (Special Section on Design Methodologies for System on a Chip) Category: Keyword: RTL verification, coverage-driven verification, sat solver, auomated testbench,
	Summary \| Full Text:PDF

Satisfiability Checking for Logic with Equality and Uninterpreted Functions under Equivalence Constraints Hiroaki KOZAWA Kiyoharu HAMAGUCHI Toshinobu KASHIWABARA
Publication: IEICE TRANSACTIONS on Fundamentals of Electronics, Communications and Computer Sciences Publication Date: 2007/12/01 Vol. E90-A No. 12 pp. 2778-2789 Type of Manuscript: Special Section PAPER (Special Section on VLSI Design and CAD Algorithms) Category: Logic Synthesis and Verification Keyword: equivalence checking, logic with equality and uninterpreted functions, equivalence constraint, satisfiability checking,
	Summary \| Full Text:PDF

Expressive Power of Quantum Pushdown Automata with Classical Stack Operations under the Perfect-Soundness Condition Masaki NAKANISHI Kiyoharu HAMAGUCHI Toshinobu KASHIWABARA
Publication: IEICE TRANSACTIONS on Information and Systems Publication Date: 2006/03/01 Vol. E89-D No. 3 pp. 1120-1127 Type of Manuscript: PAPER Category: Computation and Computational Models Keyword: quantum pushdown automata, quantum computation model, context-free-language,
	Summary \| Full Text:PDF

Symbolic Simulation Heuristics for High-Level Hardware Descriptions Including Uninterpreted Functions Kiyoharu HAMAGUCHI
Publication: IEICE TRANSACTIONS on Information and Systems Publication Date: 2004/03/01 Vol. E87-D No. 3 pp. 637-641 Type of Manuscript: Special Section LETTER (Special Section on Test and Verification of VLSI) Category: Keyword: formal verification, high-level design verification, uninterpreted function, co-design verification,
	Summary \| Full Text:PDF

Verifying Signal-Transition Consistency of High-Level Designs Based on Symbolic Simulation Kiyoharu HAMAGUCHI Hidekazu URUSHIHARA Toshinobu KASHIWABARA
Publication: IEICE TRANSACTIONS on Information and Systems Publication Date: 2002/10/01 Vol. E85-D No. 10 pp. 1587-1594 Type of Manuscript: Special Section PAPER (Special Issue on Test and Verification of VLSI) Category: Verification Keyword: formal verification, high-level design verification, uninterpreted function, co-design verification,
	Summary \| Full Text:PDF

On the Power of Non-deterministic Quantum Finite Automata Masaki NAKANISHI Takao INDOH Kiyoharu HAMAGUCHI Toshinobu KASHIWABARA
Publication: IEICE TRANSACTIONS on Information and Systems Publication Date: 2002/02/01 Vol. E85-D No. 2 pp. 327-332 Type of Manuscript: Special Section PAPER (Special Issue on Selected Papers from LA Symposium) Category: Keyword: quantum computation, quantum finite automaton, non-deterministic finite automaton, regular language,
	Summary \| Full Text:PDF

A Partially Explicit Method for Efficient Symbolic Checking of Language Containment Kiyoharu HAMAGUCHI Michiyo ICHIHARA Toshinobu KASHIWABARA
Publication: IEICE TRANSACTIONS on Fundamentals of Electronics, Communications and Computer Sciences Publication Date: 1999/11/25 Vol. E82-A No. 11 pp. 2455-2464 Type of Manuscript: Special Section PAPER (Special Section on VLSI Design and CAD Algorithms) Category: Keyword: formal verification, language containment, symbolic model checking, binary decision diagram (BDD), ω finite automaton,
	Summary \| Full Text:PDF

An Exponential Lower Bound on the Size of a Binary Moment Diagram Representing Integer Division Masaki NAKANISHI Kiyoharu HAMAGUCHI Toshinobu KASHIWABARA
Publication: IEICE TRANSACTIONS on Fundamentals of Electronics, Communications and Computer Sciences Publication Date: 1999/05/25 Vol. E82-A No. 5 pp. 756-766 Type of Manuscript: Special Section PAPER (Special Section on Discrete Mathematics and Its Applications) Category: Keyword: binary moment diagram, division, lower bound,
	Summary \| Full Text:PDF

Manipulation of Large-Scale Polynomials Using BMDs Dror ROTTER Kiyoharu HAMAGUCHI Shin-ichi MINATO Shuzo YAJIMA
Publication: IEICE TRANSACTIONS on Fundamentals of Electronics, Communications and Computer Sciences Publication Date: 1997/10/25 Vol. E80-A No. 10 pp. 1774-1781 Type of Manuscript: Special Section PAPER (Special Section on VLSI Design and CAD Algorithms) Category: Keyword: zero-suppressed binary decision diagrams (BDD), binary moment diagrams, polynomials,
	Summary \| Full Text:PDF

The Complexity of the Optimal Variable Ordering Problems of a Shared Binary Decision Diagram Seiichiro TANI Kiyoharu HAMAGUCHI Shuzo YAJIMA
Publication: IEICE TRANSACTIONS on Information and Systems Publication Date: 1996/04/25 Vol. E79-D No. 4 pp. 271-281 Type of Manuscript: PAPER Category: Algorithm and Computational Complexity Keyword: ordered binary decision diagram, variable ordering, optimal linear arrangement, NP-complete, Boolean function,
	Summary \| Full Text:PDF

Compact Test Sequences for Scan-Based Sequential Circuits Hiroyuki HIGUCHI Kiyoharu HAMAGUCHI Shuzo YAJIMA
Publication: IEICE TRANSACTIONS on Fundamentals of Electronics, Communications and Computer Sciences Publication Date: 1993/10/25 Vol. E76-A No. 10 pp. 1676-1683 Type of Manuscript: Special Section PAPER (Special Section on VLSI Design and CAD Algorithms) Category: Keyword: test generation, scan design, test application time, boolean function manipulation,
	Summary \| Full Text:PDF

Formal Design Verification of Sequential Machines Based on Symbolic Model Checking for Branching Time Regular Temporal Logic Kiyoharu HAMAGUCHI Hiromi HIRAISHI Shuzo YAJIMA
Publication: IEICE TRANSACTIONS on Fundamentals of Electronics, Communications and Computer Sciences Publication Date: 1992/10/25 Vol. E75-A No. 10 pp. 1220-1229 Type of Manuscript: Special Section PAPER (Special Section on VLSI Design and CAD Algorithms) Category: Keyword: design verification, sequential machines, temporal logic, model checking, binary decision diagram,
	Summary \| Full Text:PDF