		Search-engine friendly clone of the ACL2 documentation.

Selresolve

Vl-op-selresolve

Non-recursively resolve indices on a single select, or the multiplicity of a single multiconcat.

Signature
(vl-op-selresolve op args ss warnings context) → (mv warnings new-args)
Arguments: op — some operator being applied to args.
Guard (vl-op-p op).; args — Guard (vl-exprlist-p args).; ss — Guard (vl-scopestack-p ss).; warnings — Guard (vl-warninglist-p warnings).; context — like op(args), for better warnings.
Guard (vl-expr-p context).
Returns: warnings — Type (vl-warninglist-p warnings).; new-args — Type (vl-exprlist-p new-args).

This is the core function for simplifying indices. If op is a bit-select, part-select, or multiple concatenation, we try to evaluate expressions within it, e.g., replacing 6-1 with 5, which may have arisen during the course of unparameterization.

Definitions and Theorems

Function: vl-op-selresolve

(defun vl-op-selresolve (op args ss warnings context)
 (declare (xargs :guard (and (vl-op-p op)
                             (vl-exprlist-p args)
                             (vl-scopestack-p ss)
                             (vl-warninglist-p warnings)
                             (vl-expr-p context))))
 (declare (xargs :guard (or (not (vl-op-arity op))
                            (equal (len args) (vl-op-arity op)))))
 (let ((__function__ 'vl-op-selresolve))
  (declare (ignorable __function__))
  (b* ((op (vl-op-fix op))
       (context (vl-expr-fix context))
       (args (vl-exprlist-fix args)))
   (case
    op
    ((:vl-select-colon :vl-partselect-colon)
     (b*
      ((from (vl-expr-fix (first args)))
       (index1 (vl-expr-fix (second args)))
       (index2 (vl-expr-fix (third args)))
       ((mv ok1 index1)
        (vl-consteval index1 ss))
       ((mv ok2 index2)
        (vl-consteval index2 ss))
       ((unless (and ok1 ok2))
        (mv
         (warn
              :type :vl-bad-expression
              :msg
              "Unable to safely resolve indices on part-select ~a0."
              :args (list context))
         args))
       (msb (vl-make-index (vl-resolved->val index1)))
       (lsb (vl-make-index (vl-resolved->val index2))))
      (mv (ok) (list from msb lsb))))
    ((:vl-select-pluscolon
          :vl-partselect-pluscolon
          :vl-select-minuscolon :vl-partselect-minuscolon)
     (b*
      ((from (vl-expr-fix (first args)))
       (index1 (vl-expr-fix (second args)))
       (index2 (vl-expr-fix (third args)))
       ((mv ok1 index1)
        (vl-consteval index1 ss))
       ((mv ok2 index2)
        (vl-consteval index2 ss))
       ((unless ok2)
        (mv
         (warn
           :type :vl-bad-select
           :msg "Unable to safely resolve width on part-select ~a0."
           :args (list context))
         args))
       (new-idx1 (if ok1 (vl-make-index (vl-resolved->val index1))
                   index1))
       (new-idx2 (vl-make-index (vl-resolved->val index2))))
      (mv (ok)
          (list from new-idx1 new-idx2))))
    ((:vl-bitselect :vl-index)
     (b*
      ((from (vl-expr-fix (first args)))
       (index (vl-expr-fix (second args)))
       ((mv ok index) (vl-consteval index ss))
       ((unless ok)
        (mv
         (warn
          :type :vl-dynamic-bsel
          :msg
          "Unable to safely resolve index on bit-select ~a0, ~
                             so a dynamic bit-select will have to be used ~
                             instead."
          :args (list context))
         args))
       (atom (vl-make-index (vl-resolved->val index))))
      (mv (ok) (list from atom))))
    (:vl-multiconcat
     (b*
      ((mult (vl-expr-fix (first args)))
       (kitty (vl-expr-fix (second args)))
       ((mv ok val) (vl-consteval mult ss))
       ((unless ok)
        (mv
         (warn
          :type :vl-bad-expression
          :msg
          "Unable to safely resolve multiplicity on ~
                             multiconcat ~a0."
          :args (list context))
         args))
       ((when (>= (vl-resolved->val val) (expt 2 20)))
        (mv
         (fatal
          :type :vl-replication-too-big
          :msg
          "~a0: replicating expression with multiplicity ~
                              ~x1. That's crazy.   Causing a fatal warning to ~
                              try to prevent future transforms on this ~
                              module.  {~a2{~a3}}"
          :args (list context (vl-resolved->val val)
                      mult kitty))
         args))
       (atom (vl-make-index (vl-resolved->val val))))
      (mv (ok) (list atom kitty))))
    (otherwise (mv (ok) args))))))

Theorem: vl-warninglist-p-of-vl-op-selresolve.warnings

(defthm vl-warninglist-p-of-vl-op-selresolve.warnings
  (b* (((mv ?warnings ?new-args)
        (vl-op-selresolve op args ss warnings context)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)

Theorem: vl-exprlist-p-of-vl-op-selresolve.new-args

(defthm vl-exprlist-p-of-vl-op-selresolve.new-args
  (b* (((mv ?warnings ?new-args)
        (vl-op-selresolve op args ss warnings context)))
    (vl-exprlist-p new-args))
  :rule-classes :rewrite)

Theorem: len-of-vl-op-selresolve

(defthm len-of-vl-op-selresolve
  (implies (or (not (vl-op-arity op))
               (equal (len args) (vl-op-arity op)))
           (b* (((mv ?warnings new-args)
                 (vl-op-selresolve op args ss warnings context)))
             (equal (len new-args) (len args)))))

Theorem: vl-op-selresolve-of-vl-op-fix-op

(defthm vl-op-selresolve-of-vl-op-fix-op
  (equal (vl-op-selresolve (vl-op-fix op)
                           args ss warnings context)
         (vl-op-selresolve op args ss warnings context)))

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

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

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

(defthm vl-op-selresolve-of-vl-exprlist-fix-args
  (equal (vl-op-selresolve op (vl-exprlist-fix args)
                           ss warnings context)
         (vl-op-selresolve op args ss warnings context)))

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

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

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

(defthm vl-op-selresolve-of-vl-scopestack-fix-ss
  (equal (vl-op-selresolve op args (vl-scopestack-fix ss)
                           warnings context)
         (vl-op-selresolve op args ss warnings context)))

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

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

Theorem: vl-op-selresolve-of-vl-warninglist-fix-warnings

(defthm vl-op-selresolve-of-vl-warninglist-fix-warnings
  (equal (vl-op-selresolve op args ss (vl-warninglist-fix warnings)
                           context)
         (vl-op-selresolve op args ss warnings context)))

Theorem: vl-op-selresolve-vl-warninglist-equiv-congruence-on-warnings

(defthm vl-op-selresolve-vl-warninglist-equiv-congruence-on-warnings
  (implies
       (vl-warninglist-equiv warnings warnings-equiv)
       (equal (vl-op-selresolve op args ss warnings context)
              (vl-op-selresolve op args ss warnings-equiv context)))
  :rule-classes :congruence)

Theorem: vl-op-selresolve-of-vl-expr-fix-context

(defthm vl-op-selresolve-of-vl-expr-fix-context
  (equal (vl-op-selresolve op
                           args ss warnings (vl-expr-fix context))
         (vl-op-selresolve op args ss warnings context)))

Theorem: vl-op-selresolve-vl-expr-equiv-congruence-on-context

(defthm vl-op-selresolve-vl-expr-equiv-congruence-on-context
  (implies
       (vl-expr-equiv context context-equiv)
       (equal (vl-op-selresolve op args ss warnings context)
              (vl-op-selresolve op args ss warnings context-equiv)))
  :rule-classes :congruence)