		Search-engine friendly clone of the ACL2 documentation.

Lucid

Vl-lucidst-mark-modport

Helper function for marking interface modports as used.

Signature
(vl-lucidst-mark-modport ifname mpname ss st ctx) → new-st
Arguments: ifname — Guard (stringp ifname).; mpname — Guard (stringp mpname).; ss — Guard (vl-scopestack-p ss).; st — Guard (vl-lucidstate-p st).; ctx — Guard (vl-lucidctx-p ctx).
Returns: new-st — Type (vl-lucidstate-p new-st).

Definitions and Theorems

Function: vl-lucidst-mark-modport

(defun vl-lucidst-mark-modport (ifname mpname ss st ctx)
 (declare (xargs :guard (and (stringp ifname)
                             (stringp mpname)
                             (vl-scopestack-p ss)
                             (vl-lucidstate-p st)
                             (vl-lucidctx-p ctx))))
 (let ((__function__ 'vl-lucidst-mark-modport))
  (declare (ignorable __function__))
  (b*
   ((st (vl-lucidstate-fix st))
    (design (vl-scopestack->design ss))
    ((unless design)
     (raise
      "No design in lucid scopestack?  Something is horribly wrong.")
     st)
    (iface
         (vl-find-interface ifname (vl-design->interfaces design)))
    ((unless iface)
     (b*
      ((w
        (make-vl-warning
         :type :vl-lucid-error
         :msg
         "While marking modport in ~s0, interface port ~s1 not found."
         :args (list (with-local-ps (vl-pp-lucidctx ctx))
                     (string-fix ifname)))))
      (change-vl-lucidstate
           st
           :warnings (cons w (vl-lucidstate->warnings st)))))
    (temp-ss (vl-scopestack-init design))
    (temp-ss (vl-scopestack-push iface temp-ss))
    (temp-ss (vl-normalize-scopestack temp-ss)))
   (vl-lucid-mark-simple :used mpname temp-ss st ctx))))

Theorem: vl-lucidstate-p-of-vl-lucidst-mark-modport

(defthm vl-lucidstate-p-of-vl-lucidst-mark-modport
  (b* ((new-st (vl-lucidst-mark-modport ifname mpname ss st ctx)))
    (vl-lucidstate-p new-st))
  :rule-classes :rewrite)

Theorem: vl-lucidst-mark-modport-of-str-fix-ifname

(defthm vl-lucidst-mark-modport-of-str-fix-ifname
  (equal (vl-lucidst-mark-modport (str-fix ifname)
                                  mpname ss st ctx)
         (vl-lucidst-mark-modport ifname mpname ss st ctx)))

Theorem: vl-lucidst-mark-modport-streqv-congruence-on-ifname

(defthm vl-lucidst-mark-modport-streqv-congruence-on-ifname
 (implies
    (streqv ifname ifname-equiv)
    (equal (vl-lucidst-mark-modport ifname mpname ss st ctx)
           (vl-lucidst-mark-modport ifname-equiv mpname ss st ctx)))
 :rule-classes :congruence)

Theorem: vl-lucidst-mark-modport-of-str-fix-mpname

(defthm vl-lucidst-mark-modport-of-str-fix-mpname
  (equal (vl-lucidst-mark-modport ifname (str-fix mpname)
                                  ss st ctx)
         (vl-lucidst-mark-modport ifname mpname ss st ctx)))

Theorem: vl-lucidst-mark-modport-streqv-congruence-on-mpname

(defthm vl-lucidst-mark-modport-streqv-congruence-on-mpname
 (implies
    (streqv mpname mpname-equiv)
    (equal (vl-lucidst-mark-modport ifname mpname ss st ctx)
           (vl-lucidst-mark-modport ifname mpname-equiv ss st ctx)))
 :rule-classes :congruence)

Theorem: vl-lucidst-mark-modport-of-vl-scopestack-fix-ss

(defthm vl-lucidst-mark-modport-of-vl-scopestack-fix-ss
  (equal
       (vl-lucidst-mark-modport ifname mpname (vl-scopestack-fix ss)
                                st ctx)
       (vl-lucidst-mark-modport ifname mpname ss st ctx)))

Theorem: vl-lucidst-mark-modport-vl-scopestack-equiv-congruence-on-ss

(defthm vl-lucidst-mark-modport-vl-scopestack-equiv-congruence-on-ss
 (implies
    (vl-scopestack-equiv ss ss-equiv)
    (equal (vl-lucidst-mark-modport ifname mpname ss st ctx)
           (vl-lucidst-mark-modport ifname mpname ss-equiv st ctx)))
 :rule-classes :congruence)

Theorem: vl-lucidst-mark-modport-of-vl-lucidstate-fix-st

(defthm vl-lucidst-mark-modport-of-vl-lucidstate-fix-st
 (equal
    (vl-lucidst-mark-modport ifname mpname ss (vl-lucidstate-fix st)
                             ctx)
    (vl-lucidst-mark-modport ifname mpname ss st ctx)))

Theorem: vl-lucidst-mark-modport-vl-lucidstate-equiv-congruence-on-st

(defthm vl-lucidst-mark-modport-vl-lucidstate-equiv-congruence-on-st
 (implies
    (vl-lucidstate-equiv st st-equiv)
    (equal (vl-lucidst-mark-modport ifname mpname ss st ctx)
           (vl-lucidst-mark-modport ifname mpname ss st-equiv ctx)))
 :rule-classes :congruence)

Theorem: vl-lucidst-mark-modport-of-vl-lucidctx-fix-ctx

(defthm vl-lucidst-mark-modport-of-vl-lucidctx-fix-ctx
 (equal (vl-lucidst-mark-modport ifname
                                 mpname ss st (vl-lucidctx-fix ctx))
        (vl-lucidst-mark-modport ifname mpname ss st ctx)))

Theorem: vl-lucidst-mark-modport-vl-lucidctx-equiv-congruence-on-ctx

(defthm vl-lucidst-mark-modport-vl-lucidctx-equiv-congruence-on-ctx
 (implies
    (vl-lucidctx-equiv ctx ctx-equiv)
    (equal (vl-lucidst-mark-modport ifname mpname ss st ctx)
           (vl-lucidst-mark-modport ifname mpname ss st ctx-equiv)))
 :rule-classes :congruence)