other
(in-package "AIGNET")
other
(include-book "aignet-logic")
other
(include-book "snodes")
other
(local (include-book "arithmetic/top-with-meta" :dir :system))
other
(local (include-book "centaur/bitops/ihsext-basics" :dir :system))
other
(local (include-book "data-structures/list-defthms" :dir :system))
other
(local (in-theory (disable nth update-nth nfix-when-not-natp resize-list resize-list-when-empty make-list-ac-redef make-list-ac)))
other
(local (in-theory (disable true-listp-update-nth nth-with-large-index)))
other
(local (add-default-post-define-hook :fix))
other
(define aignet-well-formedp (aignet) :enabled t (and (node-listp aignet) (< (fanin-count aignet) 536870911) (<= (stype-count :po aignet) 536870911) (<= (stype-count :nxst aignet) 536870911) (aignet-nodes-ok aignet)))
other
(local (deffixtype aignet$a :pred aignet-well-formedp :fix node-list-fix :equiv node-list-equiv))
other
(define num-ins ((aignet aignet-well-formedp)) (stype-count (pi-stype) aignet) :enabled t)
other
(define num-regs ((aignet aignet-well-formedp)) :enabled t (stype-count (reg-stype) aignet))
other
(define num-outs ((aignet aignet-well-formedp)) (stype-count (po-stype) aignet) :enabled t)
other
(define num-nxsts ((aignet aignet-well-formedp)) (stype-count (nxst-stype) aignet) :enabled t)
other
(define num-gates ((aignet aignet-well-formedp)) (+ (stype-count (and-stype) aignet) (stype-count (xor-stype) aignet)) :enabled t)
other
(define innum->id ((n natp) (aignet aignet-well-formedp)) :guard (< n (num-ins aignet)) :returns (id natp) :enabled t (fanin-count (lookup-stype n (pi-stype) aignet)))
other
(define regnum->id ((n natp) (aignet aignet-well-formedp)) :guard (< n (num-regs aignet)) :returns (id natp) :enabled t (fanin-count (lookup-stype n (reg-stype) aignet)))
other
(define outnum->fanin ((out natp) (aignet aignet-well-formedp)) :guard (< out (num-outs aignet)) :enabled t (fanin 0 (lookup-stype out :po aignet)))
other
(define id-existsp ((id natp) (aignet aignet-well-formedp)) :enabled t (aignet-idp id aignet))
other
(defines id-phase
(define lit-phase
((lit litp) (aignet node-listp))
:guard (aignet-idp (lit->var lit)
aignet)
:verify-guards nil
:measure (two-nats-measure (lit-id lit) 1)
(b-xor (lit-neg lit)
(id-phase (lit-id lit)
aignet)))
(define id-phase
((id natp) (aignet node-listp))
:guard (aignet-idp id aignet)
:measure (two-nats-measure (nfix id) 0)
(let ((suff (lookup-id id aignet)))
(case (stype (car suff))
(:and (b-and (lit-phase (fanin 0 suff)
aignet)
(lit-phase (fanin 1 suff)
aignet)))
(:xor (b-xor (lit-phase (fanin 0 suff)
aignet)
(lit-phase (fanin 1 suff)
aignet)))
(t 0))))
///
(in-theory (disable lit-phase id-phase))
(defthm bitp-of-lit-phase
(bitp (lit-phase lit aignet))
:hints (("goal" :expand (lit-phase lit aignet))))
(defthm bitp-of-id-phase
(bitp (id-phase id aignet))
:hints (("goal" :expand (id-phase id aignet))))
(verify-guards id-phase)
(defthm-id-phase-flag (defthm id-phase-of-suffix
(implies (and (aignet-extension-p new aignet)
(<= (nfix id)
(fanin-count aignet)))
(equal (id-phase id new)
(id-phase id aignet)))
:hints ('(:expand ((:free (aignet)
(id-phase id aignet)))))
:flag id-phase)
(defthm lit-phase-of-suffix
(implies (and (aignet-extension-p new aignet)
(<= (lit-id lit)
(fanin-count aignet)))
(equal (lit-phase lit new)
(lit-phase lit aignet)))
:hints ('(:expand ((:free (aignet)
(lit-phase lit aignet)))))
:flag lit-phase))
(defthm id-phase-of-cons
(implies (<= (nfix id)
(fanin-count aignet))
(equal (id-phase id
(cons node aignet))
(id-phase id aignet)))
:hints (("goal" :use ((:instance id-phase-of-suffix
(new (cons node aignet))
(aignet aignet)))
:expand ((:free (a b)
(aignet-extension-p (cons b a)
a))))))
(defthm lit-phase-of-cons
(implies (<= (lit-id lit)
(fanin-count aignet))
(equal (lit-phase lit
(cons node aignet))
(lit-phase lit aignet)))
:hints (("goal" :use ((:instance lit-phase-of-suffix
(new (cons node aignet))
(aignet aignet)))
:expand ((:free (a b)
(aignet-extension-p (cons b a)
a))))))
(deffixequiv-mutual id-phase))
other
(define aignet-add-in^ ((aignet aignet-well-formedp)) :guard (< (num-fanins aignet) 536870911) (cons (pi-node) (node-list-fix aignet)) :enabled t /// (defthm aignet-well-formedp-of-aignet-add-in (implies (aignet-nodes-ok aignet) (aignet-nodes-ok (cons (list (pi-stype)) aignet))) :hints (("Goal" :in-theory (enable aignet-nodes-ok)))))
other
(define aignet-add-reg^ ((aignet aignet-well-formedp)) :guard (< (num-fanins aignet) 536870911) (cons (reg-node) (node-list-fix aignet)) :enabled t /// (defthm aignet-nodes-ok-of-aignet-add-reg (implies (aignet-nodes-ok aignet) (aignet-nodes-ok (cons (list (reg-stype)) aignet))) :hints (("Goal" :in-theory (enable aignet-nodes-ok)))))
other
(define aignet-add-and^
((f0 litp) (f1 litp)
(aignet aignet-well-formedp))
:guard (and (id-existsp (lit->var f0)
aignet)
(id-existsp (lit->var f1)
aignet)
(< (num-fanins aignet) 536870911))
(cons (and-node (aignet-lit-fix f0 aignet)
(aignet-lit-fix f1 aignet))
(node-list-fix aignet))
:enabled t
///
(defthm aignet-nodes-ok-of-aignet-add-and
(implies (and (aignet-nodes-ok aignet)
(id-existsp (lit->var f0)
aignet)
(id-existsp (lit->var f1)
aignet))
(aignet-nodes-ok (cons (and-node f0 f1)
aignet)))
:hints (("Goal" :in-theory (enable aignet-nodes-ok)))))
other
(define aignet-add-xor^
((f0 litp) (f1 litp)
(aignet aignet-well-formedp))
:guard (and (id-existsp (lit->var f0)
aignet)
(id-existsp (lit->var f1)
aignet)
(< (num-fanins aignet) 536870911))
(cons (xor-node (aignet-lit-fix f0 aignet)
(aignet-lit-fix f1 aignet))
(node-list-fix aignet))
:enabled t
///
(defthm aignet-nodes-ok-of-aignet-add-xor
(implies (and (aignet-nodes-ok aignet)
(id-existsp (lit->var f0)
aignet)
(id-existsp (lit->var f1)
aignet))
(aignet-nodes-ok (cons (xor-node f0 f1)
aignet)))
:hints (("Goal" :in-theory (enable aignet-nodes-ok)))))
other
(define aignet-add-out^ ((f litp) (aignet aignet-well-formedp)) :guard (and (id-existsp (lit->var f) aignet) (< (num-outs aignet) 536870910)) (cons (po-node (aignet-lit-fix f aignet)) (node-list-fix aignet)) :enabled t /// (defthm aignet-nodes-ok-of-aignet-add-out (implies (and (aignet-nodes-ok aignet) (id-existsp (lit->var f) aignet)) (aignet-nodes-ok (cons (po-node f) aignet))) :hints (("Goal" :in-theory (enable aignet-nodes-ok)))))
other
(define aignet-set-nxst^ ((f litp) (reg natp) (aignet aignet-well-formedp)) :guard (and (id-existsp (lit->var f) aignet) (< reg (num-regs aignet)) (< (num-nxsts aignet) 536870911)) (cons (nxst-node (aignet-lit-fix f aignet) reg) (node-list-fix aignet)) :enabled t /// (local (defthm equal-reg-when-stype-is-reg (implies (node-p x) (equal (equal (stype x) :reg) (equal x '(:reg)))) :hints (("Goal" :in-theory (enable node-p stype))))) (defthm aignet-nodes-ok-of-aignet-set-nxst (implies (and (aignet-nodes-ok aignet) (id-existsp (lit->var f) aignet) (< (nfix reg) (num-regs aignet))) (aignet-nodes-ok (cons (nxst-node f reg) aignet))) :hints (("Goal" :in-theory (enable aignet-nodes-ok)))))
other
(define aignet-rollback ((id posp "the num-fanins of the resulting network") (aignet aignet-well-formedp)) :guard (and (<= id (num-fanins aignet)) (equal (num-nxsts aignet) 0) (equal (num-ins aignet) (non-exec (num-ins (lookup-id (1- id) aignet)))) (equal (num-outs aignet) 0) (equal (num-regs aignet) (non-exec (num-regs (lookup-id (1- id) aignet))))) (lookup-id (1- (lposfix id)) aignet))
other
(define aignet-clear (aignet) :enabled t (declare (ignore aignet)) nil)
other
(define aignet-init^ ((max-outs :type (unsigned-byte 29)) (max-regs :type (unsigned-byte 29)) (max-ins :type (unsigned-byte 29)) (max-nodes posp :type (unsigned-byte 29)) aignet) :enabled t (declare (ignore max-outs max-regs max-ins max-nodes aignet)) nil)
other
(define create-aignet nil nil)
other
(defthm stype-cases-of-lookup-id (or (equal (stype (car (lookup-id id aignet))) :const) (equal (stype (car (lookup-id id aignet))) :pi) (equal (stype (car (lookup-id id aignet))) :reg) (equal (stype (car (lookup-id id aignet))) :and) (equal (stype (car (lookup-id id aignet))) :xor)) :hints (("Goal" :in-theory (enable lookup-id))) :rule-classes ((:forward-chaining :trigger-terms ((stype (car (lookup-id id aignet)))))))
other
(define id-slots ((id natp) (aignet aignet-well-formedp)) :guard (id-existsp id aignet) :guard-debug t :returns (mv (slot0 natp :rule-classes :type-prescription) (slot1 natp :rule-classes :type-prescription)) (b* ((suff (lookup-id id aignet))) (case (stype (car suff)) (:pi (mk-snode (in-type) 0 0 0 (stype-count :pi (cdr suff)))) (:reg (mk-snode (in-type) 1 0 (lookup-reg->nxst (stype-count :reg (cdr suff)) aignet) (stype-count :reg (cdr suff)))) (:and (mk-snode (gate-type) 0 (id-phase id aignet) (fanin 0 suff) (fanin 1 suff))) (:xor (mk-snode (gate-type) 1 (id-phase id aignet) (fanin 0 suff) (fanin 1 suff))) (t (mk-snode (const-type) 0 0 0 0)))) /// (defthm snode->type-of-id-slot (equal (snode->type (mv-nth 0 (id-slots id aignet))) (typecode (ctype (stype (car (lookup-id id aignet))))))) (defthm snode->regp-of-id-slot (equal (snode->regp (mv-nth 1 (id-slots id aignet))) (regp (stype (car (lookup-id id aignet)))))) (defthm snode->phase-of-id-slot (equal (snode->phase (mv-nth 1 (id-slots id aignet))) (id-phase id aignet)) :hints (("Goal" :in-theory (enable id-phase)))) (defthm snode->fanin-of-gate-slot (implies (equal (ctype (stype (car (lookup-id id aignet)))) :gate) (and (equal (snode->fanin (mv-nth 0 (id-slots id aignet))) (fanin 0 (lookup-id id aignet))) (equal (snode->fanin (mv-nth 1 (id-slots id aignet))) (fanin 1 (lookup-id id aignet)))))) (defthm snode->ionum-of-input (implies (equal (ctype (stype (car (lookup-id id aignet)))) :input) (equal (snode->ionum (mv-nth 1 (id-slots id aignet))) (stype-count (stype (car (lookup-id id aignet))) (cdr (lookup-id id aignet)))))) (defthm snode->fanin-of-reg (implies (equal (stype (car (lookup-id id aignet))) :reg) (equal (snode->fanin (mv-nth 0 (id-slots id aignet))) (lookup-reg->nxst (stype-count :reg (cdr (lookup-id id aignet))) aignet)))) (local (defthmd unsigned-byte-p-29-by-bound (implies (and (natp x) (<= x 536870911)) (unsigned-byte-p 29 x)))) (local (defthmd unsigned-byte-30-of-lit (implies (and (unsigned-byte-p 29 (lit->var lit)) (litp lit)) (unsigned-byte-p 30 lit)) :hints (("Goal" :in-theory (enable lit->var))))) (local (defthm unsigned-byte-30-of-aignet-lit-fix (implies (< (fanin-count aignet) 536870911) (unsigned-byte-p 30 (aignet-lit-fix lit aignet))) :hints (("Goal" :in-theory (enable fanin unsigned-byte-30-of-lit unsigned-byte-p-29-by-bound))))) (local (defthm unsigned-byte-30-of-fanin (implies (< (fanin-count aignet) 536870911) (unsigned-byte-p 30 (fanin ftype (lookup-id id aignet)))) :hints (("Goal" :in-theory (e/d (fanin) (unsigned-byte-p)))))) (local (defthm unsigned-byte-30-of-lookup-reg->nxst (implies (< (fanin-count aignet) 536870911) (unsigned-byte-p 30 (lookup-reg->nxst reg aignet))) :hints (("Goal" :in-theory (e/d (lookup-reg->nxst unsigned-byte-30-of-lit unsigned-byte-p-29-by-bound) (unsigned-byte-p)))))) (local (defthm stype-count-less-than-fanin-count (implies (not (equal (ctype stype) :output)) (<= (stype-count stype aignet) (fanin-count aignet))) :hints (("Goal" :in-theory (enable stype-count fanin-count fanin-node-p))) :rule-classes :linear)) (local (defthm unsigned-byte-30-of-stype-count (implies (and (< (fanin-count aignet) 536870911) (not (equal (ctype stype) :output))) (unsigned-byte-p 30 (stype-count stype aignet))) :hints (("Goal" :in-theory (enable unsigned-byte-p))))) (defret id-slots-unsigned-byte-p (implies (aignet-well-formedp aignet) (and (unsigned-byte-p 32 slot0) (unsigned-byte-p 32 slot1))) :hints (("Goal" :in-theory (disable unsigned-byte-p)))))