An efficient tool for system-level verification of behaviors and temporal properties