		Search-engine friendly clone of the ACL2 documentation.

Vl-consteval

Vl-clog2

Implementation of the $clog2 system function.

Signature
(vl-clog2 n) → ans
Arguments: n — Guard (natp n).
Returns: ans — Type (natp ans).

The SystemVerilog spec (20.8.1, page 567) says that $clog2(0) is 0 and that otherwise $clog2 should return the ceiling of the log base 2 of the argument, i.e., the log rounded up to an integer value.

This almost lines up with integer-length but not quite, so to avoid problems at the border cases we just need to subtract one from n. For instance:

     n      (integer-length n)     (integer-length (- n 1))    $clog2
-----------------------------------------------------------------------
     0               0                       0                   0
     1               1                       0                   0
     2               2                       1                   1
     3               2                       2                   2
     4               3                       2                   2
     5               3                       3                   3
     6               3                       3                   3
     7               3                       3                   3
     8               4                       3                   3
     9               4                       4                   4
     10              4                       4                   4
-----------------------------------------------------------------------

Definitions and Theorems

Function: vl-clog2

(defun vl-clog2 (n)
  (declare (xargs :guard (natp n)))
  (let ((__function__ 'vl-clog2))
    (declare (ignorable __function__))
    (integer-length (- (lnfix n) 1))))

Theorem: natp-of-vl-clog2

(defthm natp-of-vl-clog2
  (b* ((ans (vl-clog2 n))) (natp ans))
  :rule-classes :type-prescription)

Theorem: vl-clog2-of-nfix-n

(defthm vl-clog2-of-nfix-n
  (equal (vl-clog2 (nfix n))
         (vl-clog2 n)))

Theorem: vl-clog2-nat-equiv-congruence-on-n

(defthm vl-clog2-nat-equiv-congruence-on-n
  (implies (acl2::nat-equiv n n-equiv)
           (equal (vl-clog2 n) (vl-clog2 n-equiv)))
  :rule-classes :congruence)