• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
      • Warnings
      • Primitives
      • Use-set
      • Syntax
      • Getting-started
      • Utilities
      • Loader
      • Transforms
        • Expression-sizing
        • Occform
        • Oprewrite
        • Expand-functions
        • Delayredux
        • Unparameterization
        • Caseelim
        • Split
        • Selresolve
        • Weirdint-elim
        • Vl-delta
        • Replicate-insts
        • Rangeresolve
        • Propagate
        • Clean-selects
        • Clean-params
        • Blankargs
        • Inline-mods
        • Expr-simp
        • Trunc
        • Always-top
        • Gatesplit
        • Gate-elim
        • Expression-optimization
          • Vl-modulelist-optimize
          • Vl-op-optimize
          • Vl-expr-optimize
          • Vl-plainarglist-optimize
          • Vl-namedarglist-optimize
          • Vl-gateinstlist-optimize
          • Vl-modinstlist-optimize
          • Vl-assignlist-optimize
          • Vl-arguments-optimize
          • Vl-plainarg-optimize
          • Vl-namedarg-optimize
          • Vl-gateinst-optimize
          • Vl-assign-optimize
          • Vl-modinst-optimize
          • Vl-module-optimize
          • Vl-design-optimize
        • Elim-supplies
        • Wildelim
        • Drop-blankports
        • Clean-warnings
        • Addinstnames
        • Custom-transform-hooks
        • Annotate
        • Latchcode
        • Elim-unused-vars
        • Problem-modules
      • Lint
      • Mlib
      • Server
      • Kit
      • Printer
      • Esim-vl
      • Well-formedness
    • Sv
    • Fgl
    • Vwsim
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Expression-optimization

Vl-op-optimize

Core function in expression-optimization.

Signature

(vl-op-optimize op args ss) → new-expr?

Arguments

op — Some operator being applied to args.
    Guard (vl-op-p op).

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

ss — Stack of scopes in which this occurs.
    Guard (vl-scopestack-p ss).

Returns

new-expr? — NIL if we have no optimizations to make, or a new expression which is to replace OP(ARGS). For correctness, this new expression must be semantically equal to OP(ARGS) in this context.
    Type (equal (vl-expr-p new-expr?) (if new-expr? t nil)).

Definitions and Theorems

Function: vl-op-optimize

(defun vl-op-optimize (op args ss)
 (declare (xargs :guard (and (vl-op-p op)
                             (vl-exprlist-p args)
                             (vl-scopestack-p ss))))
 (declare (xargs :guard (or (not (vl-op-arity op))
                            (eql (len args) (vl-op-arity op)))))
 (let ((__function__ 'vl-op-optimize))
  (declare (ignorable __function__))
  (b* ((op (vl-op-fix op))
       (args (vl-exprlist-fix args)))
   (case
    op
    (:vl-bitselect
       (b* ((from (first args))
            (what (second args))
            ((unless (and (vl-idexpr-p from)
                          (vl-expr-resolved-p what)))
             nil)
            (name (vl-idexpr->name from))
            (index (vl-resolved->val what))
            ((mv successp range)
             (vl-ss-find-range name ss)))
         (cond ((not successp) nil)
               ((and (not range) (zp index)) from)
               ((and range (vl-range-resolved-p range)
                     (eql index
                          (vl-resolved->val (vl-range->msb range)))
                     (eql index
                          (vl-resolved->val (vl-range->lsb range))))
                from)
               (t nil))))
    (:vl-partselect-colon
       (b* ((from (first args))
            (left (second args))
            (right (third args))
            ((unless (and (vl-idexpr-p from)
                          (vl-expr-resolved-p left)
                          (vl-expr-resolved-p right)))
             nil)
            (name (vl-idexpr->name from))
            (l-index (vl-resolved->val left))
            (r-index (vl-resolved->val right))
            ((mv successp range)
             (vl-ss-find-range name ss)))
         (cond ((not successp) nil)
               ((and (not range)
                     (zp l-index)
                     (zp r-index))
                from)
               ((and range (vl-range-resolved-p range)
                     (eql l-index
                          (vl-resolved->val (vl-range->msb range)))
                     (eql r-index
                          (vl-resolved->val (vl-range->lsb range))))
                from)
               ((equal l-index r-index)
                (make-vl-nonatom :op :vl-bitselect
                                 :finalwidth 1
                                 :finaltype :vl-unsigned
                                 :args (list from left)))
               (t nil))))
    (otherwise nil)))))

Theorem: return-type-of-vl-op-optimize

(defthm return-type-of-vl-op-optimize
  (b* ((new-expr? (vl-op-optimize op args ss)))
    (equal (vl-expr-p new-expr?)
           (if new-expr? t nil)))
  :rule-classes :rewrite)

Theorem: vl-op-optimize-of-vl-op-fix-op

(defthm vl-op-optimize-of-vl-op-fix-op
  (equal (vl-op-optimize (vl-op-fix op) args ss)
         (vl-op-optimize op args ss)))

Theorem: vl-op-optimize-vl-op-equiv-congruence-on-op

(defthm vl-op-optimize-vl-op-equiv-congruence-on-op
  (implies (vl-op-equiv op op-equiv)
           (equal (vl-op-optimize op args ss)
                  (vl-op-optimize op-equiv args ss)))
  :rule-classes :congruence)

Theorem: vl-op-optimize-of-vl-exprlist-fix-args

(defthm vl-op-optimize-of-vl-exprlist-fix-args
  (equal (vl-op-optimize op (vl-exprlist-fix args)
                         ss)
         (vl-op-optimize op args ss)))

Theorem: vl-op-optimize-vl-exprlist-equiv-congruence-on-args

(defthm vl-op-optimize-vl-exprlist-equiv-congruence-on-args
  (implies (vl-exprlist-equiv args args-equiv)
           (equal (vl-op-optimize op args ss)
                  (vl-op-optimize op args-equiv ss)))
  :rule-classes :congruence)

Theorem: vl-op-optimize-of-vl-scopestack-fix-ss

(defthm vl-op-optimize-of-vl-scopestack-fix-ss
  (equal (vl-op-optimize op args (vl-scopestack-fix ss))
         (vl-op-optimize op args ss)))

Theorem: vl-op-optimize-vl-scopestack-equiv-congruence-on-ss

(defthm vl-op-optimize-vl-scopestack-equiv-congruence-on-ss
  (implies (vl-scopestack-equiv ss ss-equiv)
           (equal (vl-op-optimize op args ss)
                  (vl-op-optimize op args ss-equiv)))
  :rule-classes :congruence)