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 verificationcoverage-driven verificationSAT solverSMT solverautomated 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 verificationcoverage-driven verificationsat solverauomated 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 checkinglogic with equality and uninterpreted functionsequivalence constraintsatisfiability 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 automataquantum computation modelcontext-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 verificationhigh-level design verificationuninterpreted functionco-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 verificationhigh-level design verificationuninterpreted functionco-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 computationquantum finite automatonnon-deterministic finite automatonregular 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 verificationlanguage containmentsymbolic model checkingbinary 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 diagramdivisionlower 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 diagramspolynomials
 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 diagramvariable orderingoptimal linear arrangementNP-completeBoolean 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 generationscan designtest application timeboolean 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 verificationsequential machinestemporal logicmodel checkingbinary decision diagram
 Summary | Full Text:PDF