Verification of Controller Synthesis Based on Completely Specified Finite State Machine
Wei Li, Yichao Zhang, Zhengyi Liu, Jianguo Wu · 2008
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(B2/Aldrt1(n)+Aldrt2(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(Bldrt1(n) + Aldrt2(m,n)).