Formal Verification Of Controller Synthesis Based On ISSM Model

Digital systems include datapath section and controller section and so the High_level Synthesis of digital systems includes datapath synthesis and controller synthesis. The research on optimization method of controller synthesis relates to lots of theoretical problems. To solve these theoretical problems and find new practical and effective controller synthesis algorithms is one of the key problems in building usable EDA system. The correctness of controller synthesis needs to be verified. But the correctness proof of the controller synthesis result is in the relatively weak link. With the continuous increase of digital circuit scale and design optimization level, incompletely specified finite state machine (ISSM) must be used to meet the requirements and completely specified finite state machine is becomming more and more insufficient. The indeterminacy and arbitrariness of ISSM can remarkably enhance the optimization level of automatic synthesis. Whereas, the complexity of synthesis alogrithm and the difficulty of formal verification is inevitably increased. This dissertation utilizes the method of formal verification to study the correctness of controller synthesis based on ISSM and the algorithm of compatibility verificiation based on state transition graph is presented.The work and contribution of this dissertation includes:1. Studying the development of state reduction and state assignment technique, introducing efficient algorithms for state minimization of ISSM, analyzing the principle of the classic state assignment on weight targeting and its existing problem.2. Reversing annlysis from the result of controller synthesis to the behavior descripition of controller.3. Compatibility verificiation based on ISSM of behavior descripition before synthesis and behavior descripition after synthesis. The main work is:(1) First we judge the correctness of state reduction in the controller synthesis, i.e. the compatibility of STGorg and STGrd. The algorithm utilized...