Research On Verification Of Controller Synthesis In Design Automation Of Digital Systems

The EDA technology has been developing rapidly. The Top-Down Mehod in hardware design has been widely used and constantly shows its great advantages.The fundamental technique to support Top-Down design is automatic synthesis and synthesis is one of the key technologies of EDA.In order to guarantee the correctness of the result of synthesis, we must verify it.The development of automatic synthesis brings new problems to verify the correctness of hardware design.The High-Level Synthesis of Digital Systems include datapath synthesis and controller synthesis.The paper studies the correctness verification of controller synthesis based on completedly specified finite state machine and gives verification method of controller synthesis based on solving graph isomorphism problems.In order to verify controller synthesis using graph isomorphism,the paper represent the original behavior description in state transition graph-STG_org.The mutiple-input mutiput-output logic function of vertex in state transition graph represents output of related state and the single output logic function represents state transition condition; we use a 8-tuple NetList to represent the structure implement of the result of controller synthesis.This 8-tuple includes input, output, input of the state memory, output net, state transition net, state memory, output of the state memory and initial output of state memory.This paper firstly gets the equivalent behavior of the structure implement of controller through reversing the NetList,then it minimizes the state of two STGs respectively. At last,it uses graph isomorphism to determine whether the original behavior description equals to the behavior description of the result of controller or not.During the reseach, the following problems are mainly solved in my paper:(1)Reversing analysis from the result of controller synthesis to the behavior description of controller(2)Isomorphism of two State Transition Graph of Completely Specified Finite State Machines(SSMs) is provedThe following algorithms are designed in solving above problems:(1)Reversing analysis algorithm(2)Isomorphism Algorithm of two State Transition Graphs of Completely Specified Finite State MachineWe also analyse the above two algorithms in detail and their time complexity.