CEGAR-based EF synthesis of Boolean functions with an application to circuit rectification
2017
The Exists-Forall (EF) synthesis problem deals with finding parameters such that for all input assignments a correctness specification is met. Many standard problems from computer-aided design and verification can be formulated as an instance of EF synthesis when a function template with holes — parameters to be synthesized — is provided. In this paper, we generalize the idea of EF synthesis in the context of Boolean logic by allowing existential quantification over the domain of Boolean functions (rather than Boolean variables) and present a bounded synthesis approach guided by counterexamples to generate them using techniques from Boolean learning. As an application, we present circuit rectification as an EF synthesis problem and apply the presented approach to incrementally synthesize patches for digital circuits with multiple seeded faults.
Keywords:
- Electronic engineering
- Circuit minimization for Boolean functions
- Boolean expression
- Standard Boolean model
- Maximum satisfiability problem
- Boolean domain
- Boolean circuit
- And-inverter graph
- Discrete mathematics
- Product term
- Theoretical computer science
- Mathematics
- Algorithm
- Boolean function
- Computer science
- Boolean algebra
- Correction
- Source
- Cite
- Save
- Machine Reading By IdeaReader
23
References
6
Citations
NaN
KQI