Boolean functional synthesis: hardness and practical algorithms
- PDF / 1,122,639 Bytes
- 34 Pages / 439.37 x 666.142 pts Page_size
- 4 Downloads / 221 Views
Boolean functional synthesis: hardness and practical algorithms S. Akshay1 · Supratik Chakraborty1 Shetal Shah1
· Shubham Goel2 · Sumith Kulal3 ·
Received: 22 September 2019 / Accepted: 6 October 2020 © Springer Science+Business Media, LLC, part of Springer Nature 2020
Abstract Given a relational specification between Boolean inputs and outputs, Boolean functional synthesis seeks to synthesize each output as a function of the inputs such that the specification is met. Despite significant algorithmic advances in Boolean functional synthesis over the past few years, there are relatively small specifications that have remained beyond the reach of all state-of-the-art tools. In trying to understand this behaviour, we show that unless some hard conjectures in complexity theory are falsified, Boolean functional synthesis must generate large Skolem functions in the worst-case. Given this inherent hardness, what does one do to solve the problem? We present a two-phase algorithm, where the first phase is efficient in practice both in terms of time and size of synthesized functions, and solves a large fraction of our benchmarks. This phase is also guaranteed to solve the problem when the representation of the input specification satisfies some structural requirements. For those cases where the first phase doesn’t suffice, we present a second phase of our synthesis algorithm that uses a special class of algorithms, called expansion-based algorithms, to generate correct Skolem functions. This may require exponential time and generate exponential-sized Skolem functions in the worst-case. Detailed experimental evaluation shows that our overall synthesis algorithm performs better than other techniques for a large number of benchmarks. Keywords Boolean functional synthesis · Skolem functions · Expansion-based algorithms
The authors wish to acknowledge funding support from DST/CEFIPRA/INRIA Project EQuaVE and DST/SERB Matrices Grant MTR/2018/000744 for S. Akshay, and from MHRD/IMPRINT-1/Project 5496(FMSAFE) for Supratik Chakraborty and Shetal Shah. Most of this work was done when Shubham Goel and Sumith Kulal were at Indian Institute of Technology Bombay, India.
B
Supratik Chakraborty [email protected]
1
Indian Institute of Technology Bombay, Mumbai, India
2
University of California, Berkeley, USA
3
Stanford University, Stanford, USA
123
Formal Methods in System Design
1 Introduction Automatically synthesizing systems that always work as specified is one of the holy grails of computer-aided design. In many situations, it is unwieldy or even technically difficult to specify the desired behaviour of a system by expressing outputs as functions of inputs. Instead, it may be easier to specify the behaviour as a relation between inputs and outputs. Such specifications are also called relational specifications. As an interesting example, consider a system with a single 2n-bit unsigned integer input Y, and two n-bit unsigned integer outputs Z1 and Z2 . Suppose the relational specification is given as Ffact (Y, Z1 , Z2
Data Loading...
