• Top

• Sv::vl-moddb.lisp

Vlsv-aggregate-subalias

Signature

(vlsv-aggregate-subalias name width) → alias

Arguments

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

width — Guard (posp width).

Returns

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

Definitions and Theorems

Function: vlsv-aggregate-subalias

(defun vlsv-aggregate-subalias (name width)
  (declare (xargs :guard (and (sv::name-p name) (posp width))))
  (let ((__function__ 'vlsv-aggregate-subalias))
    (declare (ignorable __function__))
    (b* ((var (sv::make-simple-svar name))
         (lhs (sv::make-simple-lhs :width width
                                   :var var))
         (selfvar (sv::make-scoped-svar name :self))
         (selflhs (sv::make-simple-lhs :width width
                                       :var selfvar)))
      (list (cons lhs selflhs)))))

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

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

Theorem: vlsv-aggregate-subalias-vars

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

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

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

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

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

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

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

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

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