Embedded Systems Group (ES)

Binary Decision Diagrams

This tool offers the main BDD operations. The inputs are given as propositional formulas and are then converted to BDDs before applying the desired operation. The tool then lists the result and operand BDDs. The arguments of the particular operations are as follows:

variable ordering
first operand (bdd1)
second operand (bdd2)
variable (for compose)