Formal Verification of Unum using Theorem Proving

Adnan Rashid, Ayesha Gauhar, Osman Hasan, Sa’ed Abed and Imtiaz Ahmed
Abstract

Unum format is a 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 any inaccurate results based on these operations may lead to serious errors in hardware and software systems. To verify the computer arithmetic based on unums, this paper provides a formalization of posit, which is a type of unums. In particular, we formally model a posit format (binary encoding of a posit), which is comprised of the sign, exponent, regime and fraction bits, using the HOL Light theorem prover. In order to prove the correctness 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.