Certifying Universal Numbers (Unums) Arithmetic using Higher-order-logic Theorem Proving

Adnan Rashid
Abstract

The Universal Number (unum) format is a promising number representation format that can reduce the memory contention issues in multicore processors and parallel computing systems by providing the arithmetic operations with more efficient use of the bit storage. However, to the best of our knowledge, the accuracy of arithmetic operations based on unum has never been rigorously verified and thus a bug in these operations may lead to serious errors in hardware and software systems. To certify the computer arithmetic based on Universal Numbers (unums), this paper provides a formalization of posits, which is widely used type of unums. In particular, we formally model a posit format, which is based on the sign, exponent, regime and fraction bits, using the HOL Light theorem prover. In order to certify the formalization of a posit format, we formally verify various properties regarding conversions of a real number to a posit and a posit to a real number and the scaling factors of the regime, exponent and fraction bits of a posit using HOL Light.

Proof Script

Contact Information

Adnan Rashid is an Assistant Professor in School of Electrical Engineering and Computer Science, National University of Sciences and Technology (NUST), Pakistan.