Modeling and Implementation of Concurrent Logic Controllers with Use of Petri Nets, LSMs and Sequent Calculus

T. Gratkowski, Tkacz J., Bukowiec A., Doligalski M.

In the paper the method of modeling and implementation of concurrent controllers is presented. Concurrent controllers are specified by Petri nets. Then Petri nets are decomposed using symbolic deduction method of analysis. There are used formal methods like sequent calculus system with considered elements of Thelen’s algorithm. In the result linked state machines (LSMs) are received. Each FSM is implemented using methods of structural decomposition during process of logic synthesis. It is applied method of multiple encoding of microinstruction. It leads to decreased number of Boolean function realized by combinational part of FSM. The additional decoder could be implemented using memory blocks.