Automated generation of synchronous formal models from SystemC descriptions