查看文章

Coudert er al. have proposed in [4] an efficient method to compute the set of reachable states of a sequential finite state machine using BDD‘s. This technique can handle larger finite state machines than previously possible and has a wide range of applications in sequential synthesis, testing and verification. At the heart of this method is an algorithm that computes the range of a set of Boolean functions under a restricted domain. Coudert et al. originally proposed a simpler and more general algorithm for range computation that was based on relations, but dismissed it as impractical for all but the simplest examples. We propose a new approach based on relations that outperforms Coudert’s algorithm with the additional advantage of simplicity and wider applicability.