The BuDDy Library & Boolean Expressions

Listing 2

1:  #define WIDTH 16
2: 
3:  bdd_setvarnum( WIDTH*2 ) ;
4:  bvec a_vec = bvec_var( WIDTH, 0, 1 ) ;
5:  bvec b_vec = bvec_var( WIDTH, WIDTH, 1 ) ;
6:  bdd eq_1 = ( a_vec >= b_vec ) & ( a_vec <= b_vec ) ;
7:  bdd eq_2 = bddtrue ; // initilize eq_2 to be a constant 1
8:  for ( unsigned bit = 0 ; bit < WIDTH ; bit++ )
9:      eq_2 &= !( a_vec[ bit ] ^ b_vec[ bit ] ) ;
10: bdd eq_wrong = ( a_vec >= b_vec ) & ( a_vec < b_vec ) ;
11: // Check if the two implementations are equivalent:
12: // Output: eq_1 and eq_2 are equivalent
13: cout << "eq_1 and eq_2 are" << ( ( eq_1 != eq_2 ) ? 
14:     " not " : " " ) <<  "equivalent"  << endl ;
15: // Check again but with the wrong implementation:
16: // Output: eq_1 and eq_wrong are not equivalent
17: cout << "eq_1 and eq_wrong are" << ( ( eq_1 != eq_wrong ) ? 
18:     " not " : " " ) <<  "equivalent"  << endl ;