		Search-engine friendly clone of the ACL2 documentation.

Vl-expr-expandsizes

Vl-sign-extend-constint

(vl-sign-extend-constint value origwidth finalwidth) returns a new value, which is the sign extension of the origwidth-bit value to finalwidth bits.

Signature
(vl-sign-extend-constint value origwidth finalwidth) → *
Arguments: value — Guard (natp value).; origwidth — Guard (posp origwidth).; finalwidth — Guard (posp finalwidth).

When the MSB is true we need to add the appropriate number of 1 bits. There are probably any number of ways to do this. My method is relatively simple:

                        |---- finalwidth -------------|
                                      |-- origwidth --|
              value  == 0000...0000   1bb...bbbbbbbbbbb
  (logior)    mask   == 1111...1111   000...00000000000
----------------------------------------------------------
              result == 1111...1111   1bb...bbbbbbbbbbb

Definitions and Theorems

Function: vl-sign-extend-constint

(defun vl-sign-extend-constint (value origwidth finalwidth)
  (declare (xargs :guard (and (natp value)
                              (posp origwidth)
                              (posp finalwidth))))
  (declare (xargs :guard (and (< value (expt 2 origwidth))
                              (< origwidth finalwidth))))
  (let ((__function__ 'vl-sign-extend-constint))
    (declare (ignorable __function__))
    (b* ((msb (logbitp (1- origwidth) value))
         ((unless msb) value)
         (finalwidth-many-ones (- (expt 2 finalwidth) 1))
         (origwidth-many-ones (- (expt 2 origwidth) 1))
         (mask (logxor finalwidth-many-ones
                       origwidth-many-ones))
         (result (logior mask value)))
      result)))

Theorem: natp-of-vl-sign-extend-constint

(defthm natp-of-vl-sign-extend-constint
  (implies
       (and (force (natp value))
            (force (posp origwidth))
            (syntaxp (or (not (quotep origwidth))
                         (< (unquote origwidth) 10000)))
            (force (< value (expt 2 origwidth)))
            (force (posp finalwidth))
            (force (< origwidth finalwidth)))
       (natp (vl-sign-extend-constint value origwidth finalwidth)))
  :rule-classes :type-prescription)

Theorem: upper-bound-of-vl-sign-extend-constint

(defthm upper-bound-of-vl-sign-extend-constint
  (implies (and (force (natp value))
                (force (posp origwidth))
                (syntaxp (or (not (quotep origwidth))
                             (< (unquote origwidth) 10000)))
                (force (< value (expt 2 origwidth)))
                (force (posp finalwidth))
                (force (< origwidth finalwidth)))
           (< (vl-sign-extend-constint value origwidth finalwidth)
              (expt 2 finalwidth)))
  :rule-classes ((:rewrite) (:linear)))