Restricted branching programs and hardware verification
Stephen J. Ponzio · DSpace@MIT (Massachusetts Institute of Technology) · 1995
Recent developments in the field of digital design and hardware verification have found great use for restricted forms of branching programs. In particular, oblivious read-once branching programs (also called "OBDD's") are central to a very common technique for verifying circuits. These programs are useful because they are easily manipulated and compared for equivalence. However, their utility is limited because they cannot compute in polynomial size several simple functions---most notably, integer multiplication. This limitation has prompted the consideration of alternative models, usually restricted classes of branching programs, in the hope of finding one with greater computational power but also easily manipulated and tested for equivalence.