		Search-engine friendly clone of the ACL2 documentation.

Split

Vl-plainarg-split

Maybe split up an argument to a gate/module instances.

Signature
(vl-plainarg-split x elem delta) → (mv new-x delta)
Arguments: x — Guard (vl-plainarg-p x).; elem — Guard (vl-modelement-p elem).; delta — Guard (vl-delta-p delta).
Returns: new-x — Type (vl-plainarg-p new-x), given the guard.; delta — Type (vl-delta-p delta), given the guard.

We only want to split up expressions that are being given as inputs to submodules. If we have an output, we really want to hook up the actual wires being connected, not some new internal wire that we've just created.

This is much like how, when we split up assignments, we only split up the right-hand sides. That is, the left-hand side of an assignment is similar to a module output. We generally think it's an error for a module output to be connected to some non-sliceable expression like a + b.

I'm less sure what to do about inouts. For now I'm going to not split them up.

Definitions and Theorems

Function: vl-plainarg-split

(defun vl-plainarg-split (x elem delta)
  (declare (xargs :guard (and (vl-plainarg-p x)
                              (vl-modelement-p elem)
                              (vl-delta-p delta))))
  (let ((__function__ 'vl-plainarg-split))
    (declare (ignorable __function__))
    (b* (((vl-plainarg x) x)
         ((unless (eq x.dir :vl-input))
          (mv x delta))
         ((unless x.expr) (mv x delta))
         ((when (vl-nosplit-p x.expr))
          (mv x delta))
         ((mv new-expr delta)
          (vl-expr-split x.expr elem delta))
         (x-prime (change-vl-plainarg x :expr new-expr)))
      (mv x-prime delta))))

Theorem: vl-plainarg-p-of-vl-plainarg-split.new-x

(defthm vl-plainarg-p-of-vl-plainarg-split.new-x
  (implies (and (force (vl-plainarg-p x))
                (force (vl-modelement-p elem))
                (force (vl-delta-p delta)))
           (b* (((mv ?new-x ?delta)
                 (vl-plainarg-split x elem delta)))
             (vl-plainarg-p new-x)))
  :rule-classes :rewrite)

Theorem: vl-delta-p-of-vl-plainarg-split.delta

(defthm vl-delta-p-of-vl-plainarg-split.delta
  (implies (and (force (vl-plainarg-p x))
                (force (vl-modelement-p elem))
                (force (vl-delta-p delta)))
           (b* (((mv ?new-x ?delta)
                 (vl-plainarg-split x elem delta)))
             (vl-delta-p delta)))
  :rule-classes :rewrite)