Behavioural description of VLSI circuits based on Petri nets

The author introduces Petri net models, structural and behavioural, for CMOS circuits. The structural model is suitable for electrical and functional verification, while the behavioural model is suitable for the behavioural verification. Moreover, it is useful for analysis and synthesis of CMOS combinational logic. The extended Petri net is adopted to avoid nondeterministic behaviour and to give a functional capability to the firing rules of a transition. A systematic design methodology is described in order to provide a unified behaviour for both PMOS and NMOS transistors