Synthesis of boolean functions through binary decision diagrams

Abstract

Boolean functions are an integral component of computer science, from combinational circuits to satisfiability problems. However, although several problems can be encoded as Boolean formulas, often the most intuitive representation is not constructive but declarative, meaning that instead of a Boolean function describing how to obtain the outputs from the inputs we have a relation between Boolean inputs and outputs that must be satisfied. Although this provides a specification of the problem, in order to actually implement a circuit or program to solve it we first need a constructive function that adheres to this specification. This function can be much more complex than the specification, requiring expending time and effort in development and testing to obtain a correct imp´lementation. If we have methods to synthesize constructive implementations of Boolean functions from a declarative specification, we can automate this process and obtain correct-by-construction implementations with little human effort. In this work we propose methods to do this based on the manipulation of Binary Decision Diagrams (BDDs), a data structure for representing Boolean functions. Starting from a BDD representing the specification, we first describe how to verify that this specification defines a total function. If it is the case, we convert it into a sequence of BDDs, each representing a function that computes one of the outputs. This sequence can also be interpreted as a multi-rooted BDD, and can later be converted into a practical implementation as a circuit or program. We also tested our methods by synthesizing operations over integers in binary with varying number of bits, to observe how they scale and to obtain insights on the behavior of BDDs when used for synthesis.

Funções Booleanas são uma parte integral da ciência da computação, de circuitos combinacionais a problemas de satisfatibilidade. No entanto, apesar de diversos problemas poderem ser codificados como fórmulas Booleanas, frequentemente a representação mais intuitiva não é construtiva mas declarativa, significando que, ao invés de uma função Booleana descrevendo como obter as saídas a partir das entradas, nós temos uma relação entre entradas e saídas Booleanas que deve ser satisfeita. Apesar de tal formato fornecer uma especificação do problema, para de fato implementar um circuito ou programa para resolvê-lo precisamos primeiro de uma função construtiva que adere a essa especificação. Essa função pode ser muito mais complexa que a especificação, necessitando dispender de tempo e esforço no desenvolvimento e teste para obter uma implementação correta. Se possuirmos métodos para sintetizar implementações construtivas de funções Booleanas a partir de uma especificação declarativa, poderemos automatizar esse processo e obter implementações garantidamente corretas com mínimo esforço humano. Neste trabalho propomos métodos para realizar essa síntese baseados na manipulação de Diagramas de Decisão Binários (BDDs), uma estrutura de dados para a representação de funções Booleanas. A partir de um BDD representando a especificação, primeiro descrevemos como verificar que tal especificação define uma função total. Se é o caso, a convertemos em uma sequência de BDDs, cada um representando uma função que computa uma das saídas. Essa sequência pode também ser interpretada como um BDD de múltiplas raízes, e pode depois ser convertida em uma implementação prática na forma de um circuito ou programa. Também testamos nossos métodos sintetizando operações sobre inteiros em binário variando o número de bits, para observar sua escalabilidade e obter uma intuição sobre o comportamento de BDDs quando usados para síntese.