Embedded logic controllers specification is the first step in development process. Possible errors in this phase [1] may influence oncoming phases or even the whole venture. Usually, it generates enormous costs to remove errors which were detected too late. Dependable embedded logic controllers have additional requirements which requires beside high quality also reliability, availability, safety and secureness. Even a tiny error in design phase may change the total system behavior and may have tragic effects.

One of commonly used formal techniques by logic controllers specification are Petri Nets (PN)[2], and especially Control Interpreted Petri Nets (CIPN)[3]. They are well suited for modeling of hardware behavior including ie concurrency or resources sharing. There are many approaches to analyze CIPNs and check their boundness or liveness. There are however few approaches which allow to formally verify Petri Nets against some defined requirements, and none of them addresses directly CIPNs focused on RTL level and their behavioral specification. Model checking technique with temporal logic offers the possibility to check behavior of designed logic controller.