A PN-based approach to the high-level synthesis of digital systems

A Petri net (PN)-based approach associated with object-oriented technique is proposed to support the specification, analysis, and design of digital systems. Starting from system level to register-transfer level (RTL), the marked Petri net (MPN) with colored tokens is well applied to capture the designer's ideas and to present the system's behavior graphically. Through the net model, reachability analysis technique is employed to formally verify the digital system designed. Hence, using the behavioral properties—liveness (i.e. absence of deadlock) and safety (i.e. absence of overflow) of the net model can avoid the hardware system from deadlocks and hazards, respectively. From the live and safe MPN model we can obtain the desired hardware prototype at RTL by using the system optimization rules and object-oriented model checking. Furthermore, a time Petri net (TPN) model can be used to check the time consistency among events. This PN-based modeling approach is superior to the current techniques for requirements analysis. Finally, main results are presented in the form of four properties and supported by some experiments.