Describir: Formálna verifikácia zjemnenej špecifikácie v jazyku HSSL