Replace any blank arguments in a gate instance with fresh wires.
(vl-gateinst-plainarglist-blankargs args nf inst) → (mv new-args vardecls nf)
This is simpler than vl-modinst-plainarglist-blankargs because we do not have to consider ports: we know that every "port" of a gate exists and has size 1. We just replace any blank arguments with fresh wires of size 1.
Function:
(defun vl-gateinst-plainarglist-blankargs (args nf inst) (declare (xargs :guard (and (vl-plainarglist-p args) (vl-namefactory-p nf) (vl-gateinst-p inst)))) (let ((__function__ 'vl-gateinst-plainarglist-blankargs)) (declare (ignorable __function__)) (b* ((nf (vl-namefactory-fix nf)) (inst (vl-gateinst-fix inst)) ((when (atom args)) (mv nil nil nf)) ((mv cdr-prime cdr-vardecls nf) (vl-gateinst-plainarglist-blankargs (cdr args) nf inst)) (arg1 (vl-plainarg-fix (car args))) ((vl-plainarg arg1) arg1) ((when arg1.expr) (mv (cons arg1 cdr-prime) cdr-vardecls nf)) ((mv newname nf) (vl-namefactory-indexed-name "blank" nf)) (new-vardecl (make-vl-vardecl :name newname :type *vl-plain-old-wire-type* :nettype :vl-wire :loc (vl-gateinst->loc inst))) (new-expr (vl-idexpr newname 1 :vl-unsigned)) (arg1-prime (change-vl-plainarg arg1 :expr new-expr))) (mv (cons arg1-prime cdr-prime) (cons new-vardecl cdr-vardecls) nf))))
Theorem:
(defthm vl-plainarglist-p-of-vl-gateinst-plainarglist-blankargs.new-args (b* (((mv ?new-args ?vardecls ?nf) (vl-gateinst-plainarglist-blankargs args nf inst))) (vl-plainarglist-p new-args)) :rule-classes :rewrite)
Theorem:
(defthm vl-vardecllist-p-of-vl-gateinst-plainarglist-blankargs.vardecls (b* (((mv ?new-args ?vardecls ?nf) (vl-gateinst-plainarglist-blankargs args nf inst))) (vl-vardecllist-p vardecls)) :rule-classes :rewrite)
Theorem:
(defthm vl-namefactory-p-of-vl-gateinst-plainarglist-blankargs.nf (b* (((mv ?new-args ?vardecls ?nf) (vl-gateinst-plainarglist-blankargs args nf inst))) (vl-namefactory-p nf)) :rule-classes :rewrite)
Theorem:
(defthm vl-gateinst-plainarglist-blankargs-mvtypes-1 (true-listp (mv-nth 1 (vl-gateinst-plainarglist-blankargs args nf inst))) :rule-classes :type-prescription)
Theorem:
(defthm vl-gateinst-plainarglist-blankargs-of-vl-plainarglist-fix-args (equal (vl-gateinst-plainarglist-blankargs (vl-plainarglist-fix args) nf inst) (vl-gateinst-plainarglist-blankargs args nf inst)))
Theorem:
(defthm vl-gateinst-plainarglist-blankargs-vl-plainarglist-equiv-congruence-on-args (implies (vl-plainarglist-equiv args args-equiv) (equal (vl-gateinst-plainarglist-blankargs args nf inst) (vl-gateinst-plainarglist-blankargs args-equiv nf inst))) :rule-classes :congruence)
Theorem:
(defthm vl-gateinst-plainarglist-blankargs-of-vl-namefactory-fix-nf (equal (vl-gateinst-plainarglist-blankargs args (vl-namefactory-fix nf) inst) (vl-gateinst-plainarglist-blankargs args nf inst)))
Theorem:
(defthm vl-gateinst-plainarglist-blankargs-vl-namefactory-equiv-congruence-on-nf (implies (vl-namefactory-equiv nf nf-equiv) (equal (vl-gateinst-plainarglist-blankargs args nf inst) (vl-gateinst-plainarglist-blankargs args nf-equiv inst))) :rule-classes :congruence)
Theorem:
(defthm vl-gateinst-plainarglist-blankargs-of-vl-gateinst-fix-inst (equal (vl-gateinst-plainarglist-blankargs args nf (vl-gateinst-fix inst)) (vl-gateinst-plainarglist-blankargs args nf inst)))
Theorem:
(defthm vl-gateinst-plainarglist-blankargs-vl-gateinst-equiv-congruence-on-inst (implies (vl-gateinst-equiv inst inst-equiv) (equal (vl-gateinst-plainarglist-blankargs args nf inst) (vl-gateinst-plainarglist-blankargs args nf inst-equiv))) :rule-classes :congruence)