The paper presentes the method of modeling and implementation of concurrent controllers. Concurrent controllers are specified by Petri nets. Then Petri nets are decomposed using symbolic deduction method of analysis. Formal methods like sequent calculus system with considered elements of Thelen's algorithm have been used here. As a result, linked state machines (LSMs) are received. Each FSM is implemented using methods of structural decomposition during process of logic synthesis. The method of multiple encoding of microinstruction has been applied. It leads to decreased number of Boolean function realized by combinational part of FSM. The additional decoder could be implemented with the use of memory blocks.
The paper presents unit testing-based approach to FPGA design in-circuit verification. Presented methodology is dedicated to modular reconfigurable logic controllers, but other ip-cores and systems can be verified as well. The speed and reproducibility of tests is key for rapid system prototyping, where the quality and reliability of the system is significance. Typically FPGA are programmed by means single (full) bitstream. Specific devices are able to be reconfigured partially. Usually the partial reconfiguration is a part of the design functionality. It enables the minimization of used resources or provides specific functionality like system adaptation. The paper presents the use of the partial reconfiguration as a toll for the designer. The unit testing approach well know form software engineering was adopted to modular logic controllers development. The simulation process results waveform files, the waveform can be used for synthesizable test bench generation.
In the paper, coloring heuristic algorithm of interpreted Petri nets is presented. Coloring is used to determine the State Machines (SM) subnets. The present algorithm reduces the Petri net in order to reduce the computational complexity and finds one of its possible State Machines cover. The proposed algorithm uses elements of interpretation of Petri nets. The obtained result may not be the best, but it is sufficient for use in rapid prototyping of logic controllers. Found SM-cover will be also used in the development of algorithms for decomposition, and modular synthesis and implementation of parallel logic controllers. Correctness developed heuristic algorithm was verified using Gentzen formal reasoning system.