FORMAL REASONING IN LOGIC DESIGN OF RECONFIGURABLE CONTROLLERS

The rigorous digital design of embedded Reconfigurable Logic Controller starts from hierarchical concurrent state machine model (HCSM), which has been formally derived from modular control interpreted Petri net. The colored tokens, arcs, places and transitions distinguish nested State Machine Modules. Colored coordination places, called doubles facilitate effective and flexible Petri net state encoding. The rule based on a textual logic description of the Petri net is accepted by the hardware description language VHDL and easily mapped into Field Programmable Gate Array macrocells. Several combinatorial procedures in formal digital design of logic controller are supported by formal reasoning in the monotone Gentzen calculus.