Specifying and verifying imprecise sequential datapaths by Arithmetic Transforms