я сам не заметил улучшения времянки при использовании FSM xxxxx
поэтому не эксперт
но можно попытаться какой-нибудь formality|conformal прикрутить для поиска бага
я это никогда не делал, но, например, ксайлинс, вроде предоставляет какие-то либы для синопсиса
если получится formality - я бы ознакомился с технологией :)