Semantic embedding of Accellera PSL (Sugar) in HOL