VLDB 2026 Research / reviewers in the wild / expert
Yukio Miyasaka
dblp:240/0894
· DBLP profile ↗
10ranked-venue papers
5as first author
7since 2021 · last 2025
0000-0002-7960-9913ORCID · corroborated
Domains — the database's venue-derived domains; a paper can count in several
Systems, architecture and hardware · 10 · 5 first-author · 7 since 2021Software engineering, systems software and programming languages · 4 · 1 first-author · 3 since 2021
| Year | Publication | Venue | Position |
|---|---|---|---|
| 2025 | High-Effort Logic Synthesis Using Randomized TransductionabstractHigh-effort logic synthesis has become an important research direction due to the increase in silicon cost and the growth of design complexity. The emphasis on security leads to complex cryptographic circuits, while the acceleration of AI/ML results in custom arithmetic blocks---all of which need to be highly optimized by EDA tools. In such applications, high-effort logic synthesis allows for an efficient exploration of larger solution spaces, leading to area and power savings beyond the capacity of traditional methods. This paper presents a novel variation of high-effort logic synthesis called transduction, which performs transformation and reduction using don't-cares to restructure the circuit. Integrating the proposed method into a stochastic optimization flow with dynamic scheduling saved 6.8% AIG nodes on average, compared to the original flow using the same runtime. An additional experiment further demonstrated the strength of the proposed method, which derived smaller AIGs than the previously synthesized minimum AIGs for 46 out of 100 benchmarks. Yukio Miyasaka, Alan Mishchenko, John Wawrzynek, Dino Ruic |
ASP-DAC | 1 |
| 2025 | Bias by Design: Diversity Quantification to Mitigate Structural Bias Effects in AIG Logic OptimizationabstractAnd-Inverter Graphs (AIGs) are a fundamental data structure in logic optimization, widely used in modern electronic design automation. A persistent challenge in AIG optimization is structural bias, where the initial graph structure strongly influences optimization quality by restricting the search space, often resulting in subpar outcomes. Existing methods address this issue by running multiple optimization workflows in parallel, relying on a trial-and-error approach that lacks a systematic way to measure structural diversity or assess effectiveness, making them computationally expensive and inefficient. This paper introduces a novel framework for systematically evaluating and reducing structural bias by measuring structural diversity, defined as the degree of dissimilarity between AIG graphs. Several traditional graph similarity measures and newly proposed AIG-specific metrics, including the Rewrite, Refactor, and Resub Scores, are explored. Results reveal limitations in traditional graph similarity metrics and highlight the effectiveness of the proposed AIG-specific measures in quantifying structural dissimilarity. Notably, the RRR Score shows a strong correlation (Pearson correlation coefficient,$r$= 0.79) with post-optimization structural differences, demonstrating the reliability of the metric in capturing meaningful variations between AIG structures. This work addresses the challenge of quantifying structural bias and offers a methodology that can potentially improve optimization outcomes, with future extensions applicable to other logic graph types. Isabella Venancia Gardner, Marcel Walter, Yukio Miyasaka, Robert Wille, Michael Cochez |
DATE | 3 |
| 2024 | Transduction Method for AIG MinimizationabstractDue to the recent hike in the cost of silicon wafers, area minimization is becoming increasingly important, which makes high-effort circuit optimization more attractive, despite the additional runtime. In this paper, we revisit the transduction method originally proposed in 1980’s. The method computes don’t-cares for nodes in the circuit and iteratively performs wire reduction and other transformations. Several novel variations of the transduction method are proposed, aiming at high-effort area minimization for and-inverter graphs (AIGs) with up to one thousand nodes. These variations are applied iteratively by a script, which also performs stochastic optimization with randomized parameters. The script has been used to minimize AIGs derived from the truth tables provided at IWLS 2022 Programming Contest. In all cases, the resulting AIG sizes are the same or smaller, compared to the best results produced by the contest participants. Yukio Miyasaka |
ASPDAC | 1 |
| 2024 | Synthesis of LUT Networks for Random-Looking Dense Functions with Don't Cares - Towards Efficient FPGA Implementation of DNNabstractMany EDA applications deal with logic functions representing complex mathematical computations. Although in many cases, these functions depend on a small number of inputs, they often resemble random functions, making it hard to synthesize them using the traditional methods based on SOP minimization. This paper describes efficient synthesis and LUT mapping for this class of functions using a novel method that implements BDD-based minimization based on truth tables. The paper also investigates optimization with don't cares, when the outputs of a function are unspecified for some inputs, which is particularly useful in machine learning applications that trade accuracy for area. Compared to optimization and mapping used in academic and industrial tools, our method works faster and results in 1.5x smaller networks, while extra 20% area reduction was possible with don't cares at almost no accuracy cost. Yukio Miyasaka, Alan Mishchenko, John Wawrzynek, Nicholas J. Fraser |
FCCM | 1 |
| 2023 | Formal Verification of Integer Multiplier Circuits Using Binary Decision DiagramsabstractMultiplier circuit covers a more extensive area of embedded system application in digital signal processing, cryptography, and multimedia. Nonstandard implementations and custom optimization are being done to reduce the size of multipliers. The circuit became prone to a buggy, and hence the demand for verification increased. Formal verification methods, such as satisfiability (SAT), symbolic computer algebra (SCA), and binary decision diagrams (BDDs) have made massive progress over the last few decades. However, these methods are insufficient to verify the optimized multipliers. SAT-based equivalence checking is computationally expensive. SCA-based backward rewriting is limited to algebraic-friendly multipliers. The complexity of BDDs is exponential with the input size. Although, by allowing an additional variable method, the size of the BDD is limited to 4th degree polynomial of the number of the inputs, this method is not explored to verify optimized multipliers. This article focus on verifying integer multipliers with diverse architectures. We propose an algorithm for the direct construction of BDDs without traversing circuits and generate BDDs up to 1024 bits. We utilize the additional variable method and constructing BDDs using high-to-low variable ordering. We reduce the complexity of BDD size to a 3rd degree polynomial. We generate BDDs and verify the multipliers with various architectures up to 64 bits. We propose a method to verify optimized multipliers by checking equivalence and verifying up to 32-bits optimized multipliers. We do the error tolerance analysis of our approach by inserting bugs in a circuit at various locations. Yukio Miyasaka, Asutosh Srivastava, Masahiro Fujita 0004 |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 2 |
| 2021 | Logic Synthesis for Generalization and Learning AdditionabstractLogic synthesis generates a logic circuit of a given Boolean function, where the size and depth of the circuit are optimized for small area and low delay. On the other hand, machine learning has been extensively studied and used for many applications these days. Its general approach of training a model from a set of input-output samples is similar to logic synthesis with external don't-cares, except that in the case of machine learning the goal is to come up with a general understanding from the given samples. Seeing this resemblance from another perspective, we can think of logic synthesis targeting a generalization of the care-set. In this paper, we try such logic synthesis that generates a logic circuit where the given incomplete relation between input and output is generalized. We compared popular logic synthesis methods and machine learning models and analyzed their characteristics. We found that there were some arithmetic functions that these conventional models cannot effectively learn. Out of them, we further experimented on addition operations using tree models and found a heuristic minimization method of BDD achieves the highest accuracy. Yukio Miyasaka, Xinpei Zhang, Mingfei Yu, Qingyang Yi |
DATE | 1 |
| 2021 | Logic Synthesis Meets Machine Learning: Trading Exactness for GeneralizationabstractLogic synthesis is a fundamental step in hardware design whose goal is to find structural representations of Boolean functions while minimizing delay and area. If the function is completely-specified, the implementation accurately represents the function. If the function is incompletely-specified, the implementation has to be true only on the care set. While most of the algorithms in logic synthesis rely on SAT and Boolean methods to exactly implement the care set, we investigate learning in logic synthesis, attempting to trade exactness for generalization. This work is directly related to machine learning where the care set is the training set and the implementation is expected to generalize on a validation set. We present learning incompletely-specified functions based on the results of a competition conducted at IWLS 2020. The goal of the competition was to implement 100 functions given by a set of care minterms for training, while testing the implementation using a set of validation minterms sampled from the same function. We make this benchmark suite available and offer a detailed comparative analysis of the different approaches to learning. Shubham Rai, Walter Lau Neto, Yukio Miyasaka, Xinpei Zhang, Mingfei Yu, Qingyang Yi, Masahiro Fujita 0004, Guilherme B. Manske, Matheus F. Pontes, Leomar S. da Rosa Jr., Marilton S. de Aguiar, Paulo F. Butzen, Po-Chun Chien, Yu-Shan Huang, Hoa-Ren Wang, Jie-Hong Roland Jiang, Jiaqi Gu 0002, Zheng Zhao 0003, Zixuan Jiang, David Z. Pan, Brunno Abreu, Isac de Souza Campos, Augusto Andre Souza Berndt, Cristina Meinhardt, Jônata Tyska Carvalho, Mateus Grellert, Sergio Bampi, Aditya Lohana, Akash Kumar 0001, Wei Zeng 0015, Azadeh Davoodi, Rasit Onur Topaloglu, Jordan Dotzel, Yichi Zhang 0006, Hanyu Wang 0005, Zhiru Zhang, Valerio Tenace, Pierre-Emmanuel Gaillardon, Alan Mishchenko, Satrajit Chatterjee |
DATE | 3 |
| 2020 | Synthesis and Optimization of Multiple Portions of Circuits for ECO based on Set-Covering and QBF FormulationsabstractEngineering Change Order (ECO) and logic debugging problems where multiple locations in the circuit must be modified are formulated with Quantified Boolean Function (QBF) and set-sovering techniques. The formulation is based on the fanin selection method for each gate. Although the resulting formulation for single portion changes is basically equivalent to Sets of Pairs of Functions to be Distinguished (SPFD) [3], the way of its computations is quite different. Moreover, the simultaneous changes for multipl portions becomes Boolean Relation extension of SPFD. Experimental results and applications to various logic optimization problems are also shown. Masahiro Fujita 0004, Yusuke Kimura, Xingming Le, Yukio Miyasaka, Amir Masoud Gharehbaghi |
DATE | 4 |
| 2020 | SAT-Based Data-Flow Mapping Onto Array ProcessorabstractRecently, it has been common to perform parallel processing in machine learning. Reconfigurable array processor is drawing attention in terms of easy custom adjustment and high performance. We propose a method to map a data-flow onto an array processor using a SAT solver. The proposed method is combined with an automatic transformation method, which changes the order of calculations, to generate a more efficient computation scheme. We have solved mapping problems of matrix-vector multiplication. In our experiment, a SAT solver was more scalable than an ILP solver. Our method handled a dataflow of more than a hundred nodes using MAC operation. The automatic transformation under the associative and commutative laws is less scalable but successfully reduced calculation time. We have also mapped sparse matrix multiplication with varying latency and throughput and generated faster schedules utilizing the sparsity. Yukio Miyasaka |
VLSI-SOC | 1 |
| 2019 | Live Demonstration: Automatic Synthesis of Algorithms on Multi Chip/FPGA with Communication ConstraintsabstractMapping of large systems/computations on multiple chips/multiple cores needs sophisticated compilation methods. In this demonstration, we present our compiler tools for multi-chip and multi-core systems that considers communication architecture and the related constraints for optimal mapping. Specifically, we demonstrate compilation methods for multi-chip connected with ring topology, and multi-core connected with mesh topology, assuming fine-grained reconfigurable cores, as well as generalization techniques for large problems size as convolutional neural networks. We will demonstrate our mappings methods starting from data-flow graphs (DFGs) and equations, specifically with applications to convolutional neural networks (CNNs) for convolution layers as well as fully connected layers. Tomohiro Maruoka, Yukio Miyasaka, Akihiro Goda, Amir Masoud Gharehbaghi, Masahiro Fujita 0004 |
ISCAS | 2 |