| Hardware and software systems are evolving at a fascinating speed, thanks to the refinements of semiconductor technologies. However, verifying their correctness becomes a daunting task because of the state explosion problem. Because simulation can only validate a modern design for a fairly small portion of functional coverage, formal methods become indispensable tools in certifying design correctness. Although significant progresses have been achieved in this area, the state of the art is still far behind what is required and there is plenty room for improvement. This thesis addresses some issues in formal analysis and verification of finite state transition systems.; Through identifying some invariants, we study four subjects in the analysis and verification of finite state transition systems. First, we establish the most general definition of combinationality in designs with cyclic definitions, which occur naturally in systems specified in high-level description languages due to resource sharing, module composition, etc. This is further extended to determine the sequential determinism of systems with state holding elements. Second, we study the transformation invariants under retiming and resynthesis operations, which are the most practical techniques in the optimization of synchronous hardware systems. We characterize the optimization power of these operations and demonstrate the verification complexity of checking retiming and resynthesis equivalence. We give the rectification of initialization sequences invalidated due to these transformations. Third, we revisit equivalence checking of two finite state transition systems, which is one of the most important problems in design verification. Demonstrated is how the verification task can be fulfilled with symbolic computations in the disjoint union state space, rather than in the traditional product state space, of the two systems. Finally, because abstraction is one of the most promising techniques to leverage the state explosion problem, we investigate a reachability-preserving abstraction technique based on functional dependency. By extending combinational to sequential dependency, the detection of functional dependency can be isolated from reachability analysis. Also, our computation can be integrated into reachability analysis as an on-the-fly reduction. |
