Verification of Controller Synthesis Based on Completely Specified Finite State Machine

Controller synthesis uses hardware description language and synthesis optimization tools from a higher abstract level. State transition graph of completely specified finite state machine is adopted to describe the behavior of controller. State transition graph STG_org was generated before synthesized and state transition graph STG_ext was reversely extracted from structure realization of controller synthesis. If STG_org and STG_ext were equivalent then corresponding process of controller synthesis was correct. The paper gives a formal verification algorithm of controller synthesis with time complexity O(B²/Aldrt₁(n)+Aldrt₂(m,n)) .In order to further improve time complexity of algorithm, a verifying algorithm with synthetic information guidance was proposed. The algorithm is proved efficient in theory for its time complexity is decreased to O(Bldrt₁(n) + Aldrt₂(m,n)).