Nicholas Moore, Mark Lawford: A Case Study in the Automated Translation of BSV Hardware to PVS Formal Logic with Subsequent Verification. TASE 2022: 65-72