When X-Amin links a design, it creates a Boolean Decision Diagram (BDD) for each signal in the design. X-Amin provides several logic analysis functions which operate on the BDDs.

X-Amin also provides the capability to define your own BDDs and use these in conjunction with the BDDs in a design. User-defined BDDs can be single-bit or multi-bit structures and can be initialized when created or be defined as a top-level input.

Note that user-defined BDDs exist in the system BDD database, which is re-initialized whenever a link is performed. So, be sure to create BDDs after linking a design, otherwise they will be cleared when a design is linked.

To create a BDD, use the setbdd command:

> read mymod.v
> link
# create a BDD and set it equal to data (a signal in mymod)
> setbdd mydata data
# create a 4-bit BDD equal to the AND of signals a and b
> setbdd -size 4 myz a & b 
# plot myz
> bddplot myz

User-defined BDDs can be used in commands anywhere a linked signal can be used.

> setbdd -size 2 mycnt cnt
> prove cnt EX(mycnt==1)