(vl-datatype-elem->mod-components name subwire self-lsb submod) → (mv wire1 insts1 aliases1)
To create a wire of a given datatype, we first make the required modules and instances for the datatype, then connect up a new wire to the instance's :self wire. So if we have, e.g.,
logic [3:0] foo; struct { logic [2:0] bar; logic [1:4] baz; } fa;
then we first run vl-datatype->mods on each of the datatypes. For
the
logic [6:0] self; // representing the whole struct logic [2:0] bar; logic [1:4] baz; alias bar = self[6:4]; // aliases describe which fields correspond to which parts of self alias baz = self[3:0];
Vl-datatype->mods produces this module and returns its name (which is just the VL datatype -- call it "ourstruct" for our purposes) and its self wire.
So now, to make the wire foo, we look at the values returned by vl-datatype->mods: it still produces a self wire, even though it doesn't create a submodule, and we just modify that self wire to set the name to foo. For fa, we do the same thing, but we also create an instance of the struct module -- also named fa -- and alias the wire fa to that instance's self wire:
logic [6:0] fa; ourstruct fa (); alias fa = fa.self;
When the aliases are all composed together, this induces the right aliases for the struct:
alias fa[3:0] = fa.baz; alias fa[6:4] = fa.bar;
Sometimes we need to do this same thing for members of a struct/union or
interface. In this case, there is an additional alias that we need to
generate, mapping each vector to the (outer) self wire. This is determined by
the
Function:
(defun vl-datatype-elem->mod-components (name subwire self-lsb submod) (declare (xargs :guard (and (sv::name-p name) (sv::wire-p subwire) (maybe-natp self-lsb) (or (sv::modname-p submod) (not submod))))) (let ((__function__ 'vl-datatype-elem->mod-components)) (declare (ignorable __function__)) (b* (((sv::wire subwire)) (wire (sv::make-wire :name name :width subwire.width :low-idx subwire.low-idx)) ((unless (or submod self-lsb)) (mv wire nil nil)) ((mv insts aliases1) (if submod (b* ((modinst (sv::make-modinst :instname name :modname submod))) (mv (list modinst) (vlsv-aggregate-subalias name subwire.width))) (mv nil nil))) (aliases2 (if self-lsb (vlsv-aggregate-superalias name subwire.width self-lsb) nil))) (mv wire insts (append aliases2 aliases1)))))
Theorem:
(defthm wire-p-of-vl-datatype-elem->mod-components.wire1 (b* (((mv ?wire1 ?insts1 ?aliases1) (vl-datatype-elem->mod-components name subwire self-lsb submod))) (sv::wire-p wire1)) :rule-classes :rewrite)
Theorem:
(defthm modinstlist-p-of-vl-datatype-elem->mod-components.insts1 (b* (((mv ?wire1 ?insts1 ?aliases1) (vl-datatype-elem->mod-components name subwire self-lsb submod))) (sv::modinstlist-p insts1)) :rule-classes :rewrite)
Theorem:
(defthm lhspairs-p-of-vl-datatype-elem->mod-components.aliases1 (b* (((mv ?wire1 ?insts1 ?aliases1) (vl-datatype-elem->mod-components name subwire self-lsb submod))) (sv::lhspairs-p aliases1)) :rule-classes :rewrite)
Theorem:
(defthm vars-of-vl-datatype-elem->mod-components (b* (((mv ?wire1 ?insts1 ?aliases1) (vl-datatype-elem->mod-components name subwire self-lsb submod))) (sv::svarlist-addr-p (sv::lhspairs-vars aliases1))) :rule-classes :rewrite)
Theorem:
(defthm vl-datatype-elem->mod-components-of-name-fix-name (equal (vl-datatype-elem->mod-components (sv::name-fix name) subwire self-lsb submod) (vl-datatype-elem->mod-components name subwire self-lsb submod)))
Theorem:
(defthm vl-datatype-elem->mod-components-name-equiv-congruence-on-name (implies (sv::name-equiv name name-equiv) (equal (vl-datatype-elem->mod-components name subwire self-lsb submod) (vl-datatype-elem->mod-components name-equiv subwire self-lsb submod))) :rule-classes :congruence)
Theorem:
(defthm vl-datatype-elem->mod-components-of-wire-fix-subwire (equal (vl-datatype-elem->mod-components name (sv::wire-fix subwire) self-lsb submod) (vl-datatype-elem->mod-components name subwire self-lsb submod)))
Theorem:
(defthm vl-datatype-elem->mod-components-wire-equiv-congruence-on-subwire (implies (sv::wire-equiv subwire subwire-equiv) (equal (vl-datatype-elem->mod-components name subwire self-lsb submod) (vl-datatype-elem->mod-components name subwire-equiv self-lsb submod))) :rule-classes :congruence)
Theorem:
(defthm vl-datatype-elem->mod-components-of-maybe-natp-fix-self-lsb (equal (vl-datatype-elem->mod-components name subwire (maybe-natp-fix self-lsb) submod) (vl-datatype-elem->mod-components name subwire self-lsb submod)))
Theorem:
(defthm vl-datatype-elem->mod-components-maybe-nat-equiv-congruence-on-self-lsb (implies (acl2::maybe-nat-equiv self-lsb self-lsb-equiv) (equal (vl-datatype-elem->mod-components name subwire self-lsb submod) (vl-datatype-elem->mod-components name subwire self-lsb-equiv submod))) :rule-classes :congruence)