README
1A PRIMITIVE BDD CALCULATOR
2--------------------------
3
4This is a small program that parses commands for a BDD calculator. The
5input file contains the definition of the basic BDD variables (inputs)
6and a sequence of actions - typically assignments. The calculator can
7be used for verification of combinatorial circuits (tautology check),
8such as some of the ISCAS85 circuits in the "examples" directory. These
9ISCAS85 have been modified by another program before they where added to
10the BuDDy examples, so please do not compare the runtime results to other
11test runs.
12
13
14A BDD calculator file could be something like this ("example.cal"):
15
16 initial 100 100;
17
18 inputs
19 a b c;
20
21 actions
22 t1 = (a | b) & c;
23 t2 = (a & c) | (b & c);
24 t3 = t1 <> t2;
25 tautology t3; /* Verify that (a | b) & c == (a & c) | (b & c) */
26
27
28Where the blocks are like this:
29
30initial n c
31-----------
32 Initialize the BDD package using 'n' bddnodes and 'c' elements in
33 the caches. This part is mandatory.
34
35
36inputs id-seq
37-------------
38 Define all identifiers in the sequence 'id-seq' to be primary
39 inputs. This also corresponds to the initial BDD variable ordering,
40 starting with the first identifier in the top.
41
42
43outputs id-seq
44--------------
45 Define all identifiers in the sequence 'id-seq' to be primary
46 outputs. The sequence is space separated.
47
48
49actions act-seq
50---------------
51 A list of all the calculations and more. This list is traversed and
52 interpreted in the same order as written in the file. An action can
53 be one of the following:
54
55 Assignments: "id = expression"
56 Calculate the right-hand side and assign the value to the
57 left-hand identifier. The expression may contain:
58
59 + identifiers : A previously defined identifier
60 + true : The constant true BDD
61 + false : The constant false BDD
62 + ( ... ) : Parenteses
63 + E1 & E2 : Conjunction of two sub-expressions
64 + E1 | E2 : Disjunction of two sub-expressions
65 + E1 ^ E2 : Xor
66 + E1 => E2 : Implication
67 + E1 <> E2 : Biimplication
68 + ~E : Negation
69 + exist V.E :
70 + forall V. E : Existential/Universal quantification of the
71 variables V in the expression E. V is a space
72 separated list of input names.
73
74
75 Tautology check: "tautology id"
76 Check the variable 'id' for tautology (being equal to the constant
77 true BDD).
78
79 Size information: "size id"
80 Print the number of distinct BDD nodes used to represent 'id'.
81
82 Dump as a dot file: "dot "filename" id"
83 Dump the BDD representing 'id' as commands to the graph drawing
84 program Dot. The commands are written to the file 'filename'.
85
86 Reordering: "reorder mtd"
87 Do a dynamic variable reordering now using the method 'mtd'. The
88 argument 'mtd' may be either: win2, win2ite or sift.
89
90 Automatic reordering: "autoreorder times mtd"
91 Enable automatic dynamic variable reordering using the method
92 'mtd'. The argument 'mtd' may be either: win2, win2ite, sift or
93 none. Use none to disable automatic reordering. The 'times'
94 argument supplies the number of times that reordering may be
95 done. Use for example 1 if you only want a "one-shot" reordering.
96
97 Cache statistics: "cache"
98 Print various cache statistics for the BDD kernel.
99
100