Efficient functional verification algorithm for Petri-net-based parallel controller designs

A new algorithm for verifying the equivalence of parallel controller designs is presented along with its implementation. The controller is specified using a Petri net and its implementation is given as a netlist. The reachability graph of the Petri net is generated and simultaneously the network is implicitly simulated. By exploiting information from the reachability graph a reduction of the time and memory needed for verification has been achieved. Experimental results show that this approach is especially appropriate for parallel controller verification.