Sylvan is a parallel (multi-core) multi-terminal binary decision diagram library written in C. Sylvan implements typical binary decision diagram operations also found in libraries like CUDD, but provides scalable parallel execution of these operations and is more versatile thanks to supporting custom decision diagram terminal types. Sylvan implements parallelized operations on binary decision diagrams supporting any kind of terminal, including standard Booleans, integers, floating points and any user-defined types. Sylvan also implements operations on specialized list decision diagrams for model-checking. Both sequential and parallel BDD-based algorithms can benefit from parallelism. Sylvan uses the work-stealing framework Lace and parallel datastructures to implement scalable multi-core operations on decision diagrams. Sylvan was initially developed at the Formal Methods and Tools group at the University of Twente as part of the MaDriD project, which was funded by NWO, and further by the Formal Methods and Verification group at the Johannes Kepler University Linz as part of the RiSE project. Sylvan is licensed with the Apache 2.0 license

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element