		Search-engine friendly clone of the ACL2 documentation.

Shadowcheck

Vl-shadowcheck-interface

Signature
(vl-shadowcheck-interface x st) → (mv st new-x)
Arguments: x — Guard (vl-interface-p x).; st — Guard (vl-shadowcheck-state-p st).
Returns: st — Type (vl-shadowcheck-state-p st).; new-x — Type (vl-interface-p new-x).

Definitions and Theorems

Function: vl-shadowcheck-interface

(defun vl-shadowcheck-interface (x st)
 (declare (xargs :guard (and (vl-interface-p x)
                             (vl-shadowcheck-state-p st))))
 (let ((__function__ 'vl-shadowcheck-interface))
   (declare (ignorable __function__))
   (b*
     (((vl-interface x) (vl-interface-fix x))
      (x.loaditems (and x.parse-temps
                        (vl-parse-temps->loaditems x.parse-temps)))
      (- (vl-shadowcheck-debug "*** Shadowcheck interface ~s0 ***~%"
                               x.name))
      (warnings x.warnings)
      ((mv st warnings)
       (vl-shadowcheck-push-scope x st warnings))
      ((mv st warnings)
       (vl-shadowcheck-ports x.ports st warnings))
      ((mv st warnings)
       (vl-shadowcheck-genelementlist x.loaditems st warnings))
      (st (vl-shadowcheck-pop-scope st))
      (new-x (change-vl-interface x
                                  :warnings warnings)))
     (mv st new-x))))

Theorem: vl-shadowcheck-state-p-of-vl-shadowcheck-interface.st

(defthm vl-shadowcheck-state-p-of-vl-shadowcheck-interface.st
  (b* (((mv ?st ?new-x)
        (vl-shadowcheck-interface x st)))
    (vl-shadowcheck-state-p st))
  :rule-classes :rewrite)

Theorem: vl-interface-p-of-vl-shadowcheck-interface.new-x

(defthm vl-interface-p-of-vl-shadowcheck-interface.new-x
  (b* (((mv ?st ?new-x)
        (vl-shadowcheck-interface x st)))
    (vl-interface-p new-x))
  :rule-classes :rewrite)

Theorem: vl-shadowcheck-interface-of-vl-interface-fix-x

(defthm vl-shadowcheck-interface-of-vl-interface-fix-x
  (equal (vl-shadowcheck-interface (vl-interface-fix x)
                                   st)
         (vl-shadowcheck-interface x st)))

Theorem: vl-shadowcheck-interface-vl-interface-equiv-congruence-on-x

(defthm vl-shadowcheck-interface-vl-interface-equiv-congruence-on-x
  (implies (vl-interface-equiv x x-equiv)
           (equal (vl-shadowcheck-interface x st)
                  (vl-shadowcheck-interface x-equiv st)))
  :rule-classes :congruence)

Theorem: vl-shadowcheck-interface-of-vl-shadowcheck-state-fix-st

(defthm vl-shadowcheck-interface-of-vl-shadowcheck-state-fix-st
  (equal (vl-shadowcheck-interface x (vl-shadowcheck-state-fix st))
         (vl-shadowcheck-interface x st)))

Theorem: vl-shadowcheck-interface-vl-shadowcheck-state-equiv-congruence-on-st

(defthm
 vl-shadowcheck-interface-vl-shadowcheck-state-equiv-congruence-on-st
 (implies (vl-shadowcheck-state-equiv st st-equiv)
          (equal (vl-shadowcheck-interface x st)
                 (vl-shadowcheck-interface x st-equiv)))
 :rule-classes :congruence)