On the (non-)resetability of synchronous sequential circuits

We present a tool to compute a synchronizing sequence for synchronous sequential circuits. It consists of three parts. One part is an OBDD-based approach combined with a heuristic algorithm for preventing a memory overflow. This approach potentially finds a minimum length reset sequence. The second part is an improved three-valued based greedy algorithm. Its synchronizing sequence is not minimal in all cases, but experiments show that it is actually very good. The third part of the tool (and the focus of this paper) is a routine to quickly decide the non-resetability of a design. In contrast to previous approaches this routine is based on sufficient functional conditions to prove the non-resetability of certain memory elements. For the first time results about the resetability of the largest ISCAS´89 benchmark circuits are presented