• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
      • Warnings
      • Primitives
      • Use-set
      • Syntax
      • Getting-started
      • Utilities
      • Loader
      • Transforms
      • Lint
      • Mlib
        • Scopestack
        • Filtering-by-name
        • Vl-namefactory
        • Substitution
        • Allexprs
        • Hid-tools
        • Vl-consteval
        • Range-tools
        • Lvalexprs
        • Hierarchy
        • Finding-by-name
        • Expr-tools
        • Expr-slicing
        • Stripping-functions
        • Stmt-tools
        • Modnamespace
        • Vl-parse-expr-from-str
        • Welltyped
        • Reordering-by-name
        • Flat-warnings
        • Genblob
        • Expr-building
        • Datatype-tools
        • Syscalls
        • Relocate
        • Expr-cleaning
          • Vl-exprlist-clean-selects
          • Vl-expr-clean-selects1
          • Vl-maybe-merge-selects-aux
          • Vl-merge-consts
          • Vl-maybe-merge-selects
          • Vl-expr-clean-selects
          • Vl-elim-nested-concats
          • Vl-expr-clean-concats
        • Namemangle
        • Caremask
        • Port-tools
        • Lvalues
      • Server
      • Kit
      • Printer
      • Esim-vl
      • Well-formedness
    • Sv
    • Fgl
    • Vwsim
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Expr-cleaning

Vl-maybe-merge-selects

Merge together concatenations like {foo[3], foo[2], foo[1]} into prettier expressions like foo[3:1].

Signature

(vl-maybe-merge-selects x ss) → new-x

Arguments

x — Guard (vl-exprlist-p x).

ss — Guard (vl-scopestack-p ss).

Returns

new-x — Type (vl-exprlist-p new-x).

Here, x is a list of expressions which we assume is found within either a concatenation or a multiple concatenation. The mod and ialist are the module and its vl-make-moditem-alist so we can look up wires in x to see their ranges.

Note: to make this function more effective, x can be preprocessed with vl-elim-nested-concats.

We walk over x, looking for sequences of selects that can be merged together. For instance, foo[3:1], foo[0] could generally be merged into foo[3:0].

Definitions and Theorems

Function: vl-maybe-merge-selects

(defun vl-maybe-merge-selects (x ss)
 (declare (xargs :guard (and (vl-exprlist-p x)
                             (vl-scopestack-p ss))))
 (let ((__function__ 'vl-maybe-merge-selects))
  (declare (ignorable __function__))
  (b*
   (((when (atom x)) nil)
    (expr1 (vl-expr-fix (car x)))
    ((when (vl-fast-atom-p expr1))
     (cons expr1
           (vl-maybe-merge-selects (cdr x) ss)))
    (expr1-op (vl-nonatom->op expr1))
    ((unless (or (eq expr1-op :vl-bitselect)
                 (eq expr1-op :vl-partselect-colon)))
     (cons expr1
           (vl-maybe-merge-selects (cdr x) ss)))
    (expr1-args (vl-nonatom->args expr1))
    (expr1-from (first expr1-args))
    (expr1-high (second expr1-args))
    (expr1-low (if (eq (vl-nonatom->op expr1)
                       :vl-bitselect)
                   expr1-high
                 (third expr1-args)))
    ((unless (and (vl-idexpr-p expr1-from)
                  (vl-expr-resolved-p expr1-high)
                  (vl-expr-resolved-p expr1-low)))
     (cons expr1
           (vl-maybe-merge-selects (cdr x) ss)))
    (high-val (vl-resolved->val expr1-high))
    (low-val (vl-resolved->val expr1-low))
    ((unless (<= low-val high-val))
     (cons expr1
           (vl-maybe-merge-selects (cdr x) ss)))
    ((mv min rest)
     (vl-maybe-merge-selects-aux (cdr x)
                                 expr1-from low-val))
    ((when (= min low-val))
     (cons expr1
           (vl-maybe-merge-selects (cdr x) ss)))
    ((mv okp range)
     (vl-ss-find-range (vl-idexpr->name expr1-from)
                       ss))
    ((unless okp)
     (cons expr1
           (vl-maybe-merge-selects (cdr x) ss)))
    ((unless (and range (vl-range-resolved-p range)
                  (>= (vl-resolved->val (vl-range->msb range))
                      (vl-resolved->val (vl-range->lsb range)))
                  (>= (vl-resolved->val (vl-range->msb range))
                      high-val)
                  (>= low-val
                      (vl-resolved->val (vl-range->lsb range)))))
     (cons expr1
           (vl-maybe-merge-selects (cdr x) ss)))
    (min-expr (vl-make-index min))
    (new-expr1
        (make-vl-nonatom :op :vl-partselect-colon
                         :args (list expr1-from expr1-high min-expr)
                         :finalwidth (+ 1 (- high-val low-val))
                         :finaltype :vl-unsigned
                         :atts nil)))
   (cons new-expr1
         (vl-maybe-merge-selects rest ss)))))

Theorem: vl-exprlist-p-of-vl-maybe-merge-selects

(defthm vl-exprlist-p-of-vl-maybe-merge-selects
  (b* ((new-x (vl-maybe-merge-selects x ss)))
    (vl-exprlist-p new-x))
  :rule-classes :rewrite)

Theorem: vl-maybe-merge-selects-of-vl-exprlist-fix-x

(defthm vl-maybe-merge-selects-of-vl-exprlist-fix-x
  (equal (vl-maybe-merge-selects (vl-exprlist-fix x)
                                 ss)
         (vl-maybe-merge-selects x ss)))

Theorem: vl-maybe-merge-selects-vl-exprlist-equiv-congruence-on-x

(defthm vl-maybe-merge-selects-vl-exprlist-equiv-congruence-on-x
  (implies (vl-exprlist-equiv x x-equiv)
           (equal (vl-maybe-merge-selects x ss)
                  (vl-maybe-merge-selects x-equiv ss)))
  :rule-classes :congruence)

Theorem: vl-maybe-merge-selects-of-vl-scopestack-fix-ss

(defthm vl-maybe-merge-selects-of-vl-scopestack-fix-ss
  (equal (vl-maybe-merge-selects x (vl-scopestack-fix ss))
         (vl-maybe-merge-selects x ss)))

Theorem: vl-maybe-merge-selects-vl-scopestack-equiv-congruence-on-ss

(defthm vl-maybe-merge-selects-vl-scopestack-equiv-congruence-on-ss
  (implies (vl-scopestack-equiv ss ss-equiv)
           (equal (vl-maybe-merge-selects x ss)
                  (vl-maybe-merge-selects x ss-equiv)))
  :rule-classes :congruence)