		Search-engine friendly clone of the ACL2 documentation.

Features

Feat->xnum

The number of x registers.

Signature
(feat->xnum feat) → xnum
Arguments: feat — Guard (featp feat).
Returns: xnum — Type (posp xnum).

These is 32 for the RV32I and RV64I bases, but it is reduced to 16 for the RV32E and RV64E bases [ISA:3]. Although our features do not yet model the latter bases, we define this operation so that other code can use it and more easily accommodate the extension for RV32E/RV64E.

Definitions and Theorems

Function: feat->xnum

(defun feat->xnum (feat)
  (declare (xargs :guard (featp feat)))
  (declare (ignore feat))
  (let ((__function__ 'feat->xnum))
    (declare (ignorable __function__))
    32))

Theorem: posp-of-feat->xnum

(defthm posp-of-feat->xnum
  (b* ((xnum (feat->xnum feat)))
    (posp xnum))
  :rule-classes :rewrite)

Theorem: feat->xnum-of-feat-fix-feat

(defthm feat->xnum-of-feat-fix-feat
  (equal (feat->xnum (feat-fix feat))
         (feat->xnum feat)))

Theorem: feat->xnum-feat-equiv-congruence-on-feat

(defthm feat->xnum-feat-equiv-congruence-on-feat
  (implies (feat-equiv feat feat-equiv)
           (equal (feat->xnum feat)
                  (feat->xnum feat-equiv)))
  :rule-classes :congruence)