A framework for assertion-based timing verification and PC-based restbus simulation of automotive systems