Showing 1–8 of 8 results for author: Riener, H

An Automated Testing and Debugging Toolkit for Gate-Level Logic Synthesis Applications

Authors: Siang-Yun Lee, Heinz Riener, Giovanni De Micheli

Abstract: Correctness and robustness are essential for logic synthesis applications, but they are often only tested with a limited set of benchmarks. Moreover, when the application fails on a large benchmark, the debugging process may be tedious and time-consuming. In some fields such as compiler construction, automatic testing and debugging tools are well-developed to support developers and provide minimal… ▽ More Correctness and robustness are essential for logic synthesis applications, but they are often only tested with a limited set of benchmarks. Moreover, when the application fails on a large benchmark, the debugging process may be tedious and time-consuming. In some fields such as compiler construction, automatic testing and debugging tools are well-developed to support developers and provide minimal guarantees on program quality. In this paper, we adapt fuzz testing and delta debugging techniques and specialize them for gate-level netlists commonly used in logic synthesis. Our toolkit improves over similar tools specialized for the AIGER format by supporting other gate-level netlist formats and by allowing a tight integration to provide 10x speed-up. Experimental results show that our fuzzer captures defects in mockturtle, ABC, and LSOracle with 10x smaller testcases and our testcase minimizer extracts minimal failure-inducing cores using 2x fewer oracle calls. △ Less

Submitted 17 July, 2022; originally announced July 2022.

Comments: originally accepted at Int'l Workshop on Logic & Synthesis 2022

Irredundant Buffer and Splitter Insertion and Scheduling-Based Optimization for AQFP Circuits

Authors: Siang-Yun Lee, Heinz Riener, Giovanni De Micheli

Abstract: The adiabatic quantum-flux parametron (AQFP) is a promising energy-efficient superconducting technology. Before technology map**, additional buffer and splitter cells need to be inserted into AQFP circuits to fulfill two special constraints: (1) Input signals to a logic gate need to arrive at the same time, thus shorter paths need to be delayed with buffers. (2) The output signal of a logic gate… ▽ More The adiabatic quantum-flux parametron (AQFP) is a promising energy-efficient superconducting technology. Before technology map**, additional buffer and splitter cells need to be inserted into AQFP circuits to fulfill two special constraints: (1) Input signals to a logic gate need to arrive at the same time, thus shorter paths need to be delayed with buffers. (2) The output signal of a logic gate has to be actively branched with splitters if it drives multiple fanouts. Buffers and splitters largely increase the area and delay in AQFP circuits. Naïve buffer and splitter insertion and light-weight optimization using retiming techniques have been used in related works, and it is not clear how much space there is for further optimization. In this paper, we develop (a) a linear-time algorithm to insert buffers and splitters irredundantly, and (b) optimization methods by scheduling and by moving groups of gates, called chunks, together. Experimental results show a reduction of up to 39% on buffer and splitter cost. Moreover, as the technology is still develo** and assumptions on the physical constraints are not clear yet, we also discuss the impacts of different assumptions with experimental results to motivate future research on AQFP register design. △ Less

Submitted 1 September, 2021; originally announced September 2021.

Comments: originally accepted at Int'l Workshop on Logic & Synthesis 2021

Safety Synthesis Sans Specification

Authors: Roderick Bloem, Hana Chockler, Masoud Ebrahimi, Dana Fisman, Heinz Riener

Abstract: We define the problem of learning a transducer ${S}$ from a target language $U$ containing possibly conflicting transducers, using membership queries and conjecture queries. The requirement is that the language of ${S}$ be a subset of $U$. We argue that this is a natural question in many situations in hardware and software verification. We devise a learning algorithm for this problem and show that… ▽ More We define the problem of learning a transducer ${S}$ from a target language $U$ containing possibly conflicting transducers, using membership queries and conjecture queries. The requirement is that the language of ${S}$ be a subset of $U$. We argue that this is a natural question in many situations in hardware and software verification. We devise a learning algorithm for this problem and show that its time and query complexity is polynomial with respect to the rank of the target language, its incompatibility measure, and the maximal length of a given counterexample. We report on experiments conducted with a prototype implementation. △ Less

Submitted 27 November, 2020; v1 submitted 15 November, 2020; originally announced November 2020.

Simulation-Guided Boolean Resubstitution

Authors: Siang-Yun Lee, Heinz Riener, Alan Mishchenko, Robert K. Brayton, Giovanni De Micheli

Abstract: This paper proposes a new logic optimization paradigm based on circuit simulation, which reduces the need for Boolean computations such as SAT-solving or constructing BDDs. The paper develops a Boolean resubstitution framework to demonstrate the effectiveness of the proposed approach. Methods to generate highly expressive simulation patterns are developed, and the generated patterns are used in re… ▽ More This paper proposes a new logic optimization paradigm based on circuit simulation, which reduces the need for Boolean computations such as SAT-solving or constructing BDDs. The paper develops a Boolean resubstitution framework to demonstrate the effectiveness of the proposed approach. Methods to generate highly expressive simulation patterns are developed, and the generated patterns are used in resubstitution for efficient filtering of potential resubstitution candidates to reduce the need for SAT validation. Experimental results show that improvements in circuit size reduction were achieved by up to 74%, compared to a state-of-the-art resubstitution algorithm. △ Less

Submitted 6 July, 2020; originally announced July 2020.

Comments: 8 pages, originally accepted at Int'l Workshop on Logic & Synthesis 2020

Synthesizing Adaptive Test Strategies from Temporal Logic Specifications

Authors: Roderick Bloem, Goerschwin Fey, Fabian Greif, Robert Koenighofer, Ingo Pill, Heinz Riener, Franz Roeck

Abstract: Constructing good test cases is difficult and time-consuming, especially if the system under test is still under development and its exact behavior is not yet fixed. We propose a new approach to compute test strategies for reactive systems from a given temporal logic specification using formal methods. The computed strategies are guaranteed to reveal certain simple faults in every realization of t… ▽ More Constructing good test cases is difficult and time-consuming, especially if the system under test is still under development and its exact behavior is not yet fixed. We propose a new approach to compute test strategies for reactive systems from a given temporal logic specification using formal methods. The computed strategies are guaranteed to reveal certain simple faults in every realization of the specification and for every behavior of the uncontrollable part of the system's environment. The proposed approach supports different assumptions on occurrences of faults (ranging from a single transient fault to a persistent fault) and by default aims at unveiling the weakest one. Based on well-established hypotheses from fault-based testing, we argue that such tests are also sensitive for more complex bugs. Since the specification may not define the system behavior completely, we use reactive synthesis algorithms with partial information. The computed strategies are adaptive test strategies that react to behavior at runtime. We work out the underlying theory of adaptive test strategy synthesis and present experiments for a safety-critical component of a real-world satellite system. We demonstrate that our approach can be applied to industrial specifications and that the synthesized test strategies are capable of detecting bugs that are hard to detect with random testing. △ Less

Submitted 5 September, 2018; originally announced September 2018.

Exact Synthesis of ESOP Forms

Authors: Heinz Riener, Rüdiger Ehlers, Bruno Schmitt, Giovanni De Micheli

Abstract: We present an exact synthesis approach for computing Exclusive-or Sum-of-Products (ESOP) forms with a minimum number of product terms using Boolean satisfiability. Our approach finds one or more ESOP forms for a given Boolean function. The approach can deal with incompletely-specified Boolean functions defined over many Boolean variables and is particularly fast if the Boolean function can be expr… ▽ More We present an exact synthesis approach for computing Exclusive-or Sum-of-Products (ESOP) forms with a minimum number of product terms using Boolean satisfiability. Our approach finds one or more ESOP forms for a given Boolean function. The approach can deal with incompletely-specified Boolean functions defined over many Boolean variables and is particularly fast if the Boolean function can be expressed with only a few product terms. We describe the formalization of the ESOP synthesis problem with a fixed number of terms as a decision problem and present search procedures for determining ESOP forms of minimum size. We further discuss how the search procedures can be relaxed to find ESOP forms of small sizes in reasonable time. We experimentally evaluate the performance of the SAT-based synthesis procedures on completely- and incompletely-specified Boolean functions. △ Less

Submitted 29 July, 2018; originally announced July 2018.

Comments: 16 pages, accepted at 13th Int'l Workshop on Boolean Problems

The EPFL Logic Synthesis Libraries

Authors: Mathias Soeken, Heinz Riener, Winston Haaswijk, Eleonora Testa, Bruno Schmitt, Giulia Meuli, Fereshte Mozafari, Siang-Yun Lee, Alessandro Tempia Calvino, Dewmini Sudara Marakkalage, Giovanni De Micheli

Abstract: We present a collection of modular open source C++ libraries for the development of logic synthesis applications. These libraries can be used to develop applications for the design of classical and emerging technologies, as well as for the implementation of quantum compilers. All libraries are well documented and well tested. Furthermore, being header-only, the libraries can be readily used as cor… ▽ More We present a collection of modular open source C++ libraries for the development of logic synthesis applications. These libraries can be used to develop applications for the design of classical and emerging technologies, as well as for the implementation of quantum compilers. All libraries are well documented and well tested. Furthermore, being header-only, the libraries can be readily used as core components in complex logic synthesis systems. △ Less

Submitted 3 June, 2022; v1 submitted 14 May, 2018; originally announced May 2018.

Comments: 13 pages, originally accepted at Int'l Workshop on Logic & Synthesis 2018, extended for Workshop on Open-Source EDA Technology 2019

Path-Based Program Repair

Authors: Heinz Riener, Rüdiger Ehlers, Görschwin Fey

Abstract: We propose a path-based approach to program repair for imperative programs. Our repair framework takes as input a faulty program, a logic specification that is refuted, and a hint where the fault may be located. An iterative abstraction refinement loop is then used to repair the program: in each iteration, the faulty program part is re-synthesized considering a symbolic counterexample, where the c… ▽ More We propose a path-based approach to program repair for imperative programs. Our repair framework takes as input a faulty program, a logic specification that is refuted, and a hint where the fault may be located. An iterative abstraction refinement loop is then used to repair the program: in each iteration, the faulty program part is re-synthesized considering a symbolic counterexample, where the control-flow is kept concrete but the data-flow is symbolic. The appeal of the idea is two-fold: 1) the approach lazily considers candidate repairs and 2) the repairs are directly derived from the logic specification. In contrast to prior work, our approach is complete for programs with finitely many control-flow paths, i.e., the program is repaired if and only if it can be repaired at the specified fault location. Initial results for small programs indicate that the approach is useful for debugging programs in practice. △ Less

Submitted 16 March, 2015; originally announced March 2015.

Comments: In Proceedings FESCA 2015, arXiv:1503.04378

Journal ref: EPTCS 178, 2015, pp. 22-32