ROBDDs application for finding the shortest transfer sequence of sequential circuit or only revealing existence of this sequence without deriving the sequence itself
Anzhela Yu. Matrosova, Valentina Vladimirovna Andreeva, A. Melnikov · 2016
Methods of revealing of transfer sequence existence of the length not more l for a set of states (internal states) without deriving the sequence itself and finding the shortest transfer sequence of the length not more l for a sequential circuit are developed. The methods are based on applying operations either on full ROBDDs, representing transition functions or fragments of these ROBDDs. Multiplications of the proper ROBDDs are executed with using full ROBDDs but summations - with using ROBDDs fragments. It is setup that for revealing transfer sequence existence we may use ROBDDs fragments depending on only state variables. When finding the shortest sequence we use ROBDDs so that each path originated by state variables has the only prolongation among input variables. The initial state of a sequential circuit is given. Set M0of states one of which has to be reached is represented by the ROBDD.