• Top

• Sv::vl-moddb.lisp

Vlsv-aggregate-superalias

Signature

(vlsv-aggregate-superalias name width lsb) → alias

Arguments

name — Guard (sv::name-p name).

width — Guard (posp width).

lsb — Guard (natp lsb).

Returns

alias — Type (sv::lhspairs-p alias).

Definitions and Theorems

Function: vlsv-aggregate-superalias

(defun vlsv-aggregate-superalias (name width lsb)
  (declare (xargs :guard (and (sv::name-p name)
                              (posp width)
                              (natp lsb))))
  (let ((__function__ 'vlsv-aggregate-superalias))
    (declare (ignorable __function__))
    (b* ((var (sv::make-simple-svar name))
         (lhs (sv::make-simple-lhs :width width
                                   :var var))
         (outervar (sv::make-simple-svar :self))
         (outerlhs (sv::make-simple-lhs :width width
                                        :var outervar
                                        :rsh lsb)))
      (list (cons lhs outerlhs)))))

Theorem: lhspairs-p-of-vlsv-aggregate-superalias

(defthm lhspairs-p-of-vlsv-aggregate-superalias
  (b* ((alias (vlsv-aggregate-superalias name width lsb)))
    (sv::lhspairs-p alias))
  :rule-classes :rewrite)

Theorem: vlsv-aggregate-superalias-vars

(defthm vlsv-aggregate-superalias-vars
  (b* ((?alias (vlsv-aggregate-superalias name width lsb)))
    (sv::svarlist-addr-p (sv::lhspairs-vars alias))))

Theorem: vlsv-aggregate-superalias-of-name-fix-name

(defthm vlsv-aggregate-superalias-of-name-fix-name
  (equal (vlsv-aggregate-superalias (sv::name-fix name)
                                    width lsb)
         (vlsv-aggregate-superalias name width lsb)))

Theorem: vlsv-aggregate-superalias-name-equiv-congruence-on-name

(defthm vlsv-aggregate-superalias-name-equiv-congruence-on-name
  (implies (sv::name-equiv name name-equiv)
           (equal (vlsv-aggregate-superalias name width lsb)
                  (vlsv-aggregate-superalias name-equiv width lsb)))
  :rule-classes :congruence)

Theorem: vlsv-aggregate-superalias-of-pos-fix-width

(defthm vlsv-aggregate-superalias-of-pos-fix-width
  (equal (vlsv-aggregate-superalias name (pos-fix width)
                                    lsb)
         (vlsv-aggregate-superalias name width lsb)))

Theorem: vlsv-aggregate-superalias-pos-equiv-congruence-on-width

(defthm vlsv-aggregate-superalias-pos-equiv-congruence-on-width
  (implies (acl2::pos-equiv width width-equiv)
           (equal (vlsv-aggregate-superalias name width lsb)
                  (vlsv-aggregate-superalias name width-equiv lsb)))
  :rule-classes :congruence)

Theorem: vlsv-aggregate-superalias-of-nfix-lsb

(defthm vlsv-aggregate-superalias-of-nfix-lsb
  (equal (vlsv-aggregate-superalias name width (nfix lsb))
         (vlsv-aggregate-superalias name width lsb)))

Theorem: vlsv-aggregate-superalias-nat-equiv-congruence-on-lsb

(defthm vlsv-aggregate-superalias-nat-equiv-congruence-on-lsb
  (implies (acl2::nat-equiv lsb lsb-equiv)
           (equal (vlsv-aggregate-superalias name width lsb)
                  (vlsv-aggregate-superalias name width lsb-equiv)))
  :rule-classes :congruence)