Combining ACL2 and an automated verification tool to verify a multiplierErik ReeberJun Sawada2006ACL2 2006