		Search-engine friendly clone of the ACL2 documentation.

Compile.lisp

Svex-design-flatten

Signature
(svex-design-flatten x &key (moddb 'moddb) (aliases 'aliases)) → (mv err flat-assigns flat-fixups flat-constraints new-moddb new-aliases)
Arguments: x — Guard (design-p x).; moddb — overwritten.; aliases — overwritten.
Returns: flat-assigns — Type (assigns-p flat-assigns).; flat-fixups — Type (assigns-p flat-fixups).; flat-constraints — Type (constraintlist-p flat-constraints).; new-moddb — Type (and (moddb-basics-ok new-moddb) (moddb-mods-ok new-moddb)).; new-aliases — Type (implies (not err) (aliases-normorderedp new-aliases)).

Definitions and Theorems

Function: svex-design-flatten-fn

(defun svex-design-flatten-fn (x moddb aliases)
 (declare (xargs :stobjs (moddb aliases)))
 (declare (xargs :guard (design-p x)))
 (declare
  (xargs
     :guard (svarlist-addr-p (modalist-vars (design->modalist x)))))
 (let ((__function__ 'svex-design-flatten))
  (declare (ignorable __function__))
  (b*
   ((moddb (moddb-clear moddb))
    (aliases (resize-lhss 0 aliases))
    ((design x) x)
    (modalist x.modalist)
    (topmod x.top)
    ((with-fast modalist))
    ((unless (cwtime (modhier-loopfree-p topmod modalist)
                     :mintime 1))
     (mv (msg "Module ~s0 has an instance loop!~%"
              topmod)
         nil nil nil moddb aliases))
    (moddb (cwtime (module->db topmod modalist moddb)
                   :mintime 1))
    (modidx (moddb-modname-get-index topmod moddb))
    ((stobj-get totalwires)
     ((elab-mod (moddb->modsi modidx moddb)))
     (elab-mod->totalwires elab-mod))
    (aliases (resize-lhss totalwires aliases))
    ((mv err modalist)
     (cwtime (modalist-named->indexed modalist moddb
                                      :quiet t)
             :mintime 1))
    ((when err)
     (mv (msg "Error indexing wire names: ~@0~%" err)
         nil nil nil moddb aliases))
    ((with-fast modalist))
    (scope (make-modscope-top :modidx modidx))
    ((mv varfails
         modfails flat-aliases flat-assigns
         flat-fixups flat-constraints)
     (cwtime (svex-mod->flatten scope modalist moddb)
             :mintime 1))
    ((when modfails)
     (mv (msg "Module names referenced but not found: ~x0~%"
              (cap-length 20 modfails))
         nil nil nil moddb aliases))
    ((when varfails)
     (mv (msg "Variable names malformed/unresolved: ~x0~%"
              (cap-length 20 varfails))
         nil nil nil moddb aliases))
    (aliases
         (cwtime (svex-mod->initial-aliases modidx 0 moddb aliases)
                 :mintime 1))
    (aliases (cwtime (canonicalize-alias-pairs flat-aliases aliases)
                     :mintime 1)))
   (mv nil flat-assigns flat-fixups
       flat-constraints moddb aliases))))

Theorem: assigns-p-of-svex-design-flatten.flat-assigns

(defthm assigns-p-of-svex-design-flatten.flat-assigns
  (b* (((mv ?err ?flat-assigns
            ?flat-fixups ?flat-constraints
            ?new-moddb ?new-aliases)
        (svex-design-flatten-fn x moddb aliases)))
    (assigns-p flat-assigns))
  :rule-classes :rewrite)

Theorem: assigns-p-of-svex-design-flatten.flat-fixups

(defthm assigns-p-of-svex-design-flatten.flat-fixups
  (b* (((mv ?err ?flat-assigns
            ?flat-fixups ?flat-constraints
            ?new-moddb ?new-aliases)
        (svex-design-flatten-fn x moddb aliases)))
    (assigns-p flat-fixups))
  :rule-classes :rewrite)

Theorem: constraintlist-p-of-svex-design-flatten.flat-constraints

(defthm constraintlist-p-of-svex-design-flatten.flat-constraints
  (b* (((mv ?err ?flat-assigns
            ?flat-fixups ?flat-constraints
            ?new-moddb ?new-aliases)
        (svex-design-flatten-fn x moddb aliases)))
    (constraintlist-p flat-constraints))
  :rule-classes :rewrite)

Theorem: return-type-of-svex-design-flatten.new-moddb

(defthm return-type-of-svex-design-flatten.new-moddb
  (b* (((mv ?err ?flat-assigns
            ?flat-fixups ?flat-constraints
            ?new-moddb ?new-aliases)
        (svex-design-flatten-fn x moddb aliases)))
    (and (moddb-basics-ok new-moddb)
         (moddb-mods-ok new-moddb)))
  :rule-classes :rewrite)

Theorem: return-type-of-svex-design-flatten.new-aliases

(defthm return-type-of-svex-design-flatten.new-aliases
  (b* (((mv ?err ?flat-assigns
            ?flat-fixups ?flat-constraints
            ?new-moddb ?new-aliases)
        (svex-design-flatten-fn x moddb aliases)))
    (implies (not err)
             (aliases-normorderedp new-aliases)))
  :rule-classes :rewrite)

Theorem: alias-length-of-svex-design-flatten

(defthm alias-length-of-svex-design-flatten
 (b* (((mv ?err ?flat-assigns
           ?flat-fixups ?flat-constraints
           ?new-moddb ?new-aliases)
       (svex-design-flatten-fn x moddb aliases)))
  (implies
   (not err)
   (equal
      (len new-aliases)
      (moddb-mod-totalwires (moddb-modname-get-index (design->top x)
                                                     new-moddb)
                            new-moddb)))))

Theorem: modidx-of-svex-design-flatten

(defthm modidx-of-svex-design-flatten
 (b* (((mv ?err ?flat-assigns
           ?flat-fixups ?flat-constraints
           ?new-moddb ?new-aliases)
       (svex-design-flatten-fn x moddb aliases)))
   (implies (not err)
            (moddb-modname-get-index (design->top x)
                                     new-moddb)))
 :rule-classes
 (:rewrite
  (:type-prescription
   :corollary
   (implies
    (not (mv-nth 0
                 (svex-design-flatten-fn x moddb aliases)))
    (natp
        (moddb-modname-get-index
             (design->top x)
             (mv-nth 4
                     (svex-design-flatten-fn x moddb aliases))))))))

Theorem: assigns-boundedp-of-svex-design-flatten

(defthm assigns-boundedp-of-svex-design-flatten
 (b* (((mv ?err ?flat-assigns
           ?flat-fixups ?flat-constraints
           ?new-moddb ?new-aliases)
       (svex-design-flatten-fn x moddb aliases)))
  (b*
   ((bound
      (moddb-mod-totalwires (moddb-modname-get-index (design->top x)
                                                     new-moddb)
                            new-moddb)))
   (and (svarlist-boundedp (assigns-vars flat-assigns)
                           bound)
        (svarlist-boundedp (constraintlist-vars flat-constraints)
                           bound)
        (svarlist-boundedp (assigns-vars flat-fixups)
                           bound)))))

Theorem: normalize-stobjs-of-svex-design-flatten

(defthm normalize-stobjs-of-svex-design-flatten
  (b* nil
    (implies (syntaxp (not (and (equal aliases ''nil)
                                (equal moddb ''nil))))
             (equal (svex-design-flatten-fn x moddb aliases)
                    (let ((moddb nil) (aliases nil))
                      (svex-design-flatten-fn x moddb aliases))))))

Theorem: svex-design-flatten-fn-of-design-fix-x

(defthm svex-design-flatten-fn-of-design-fix-x
  (equal (svex-design-flatten-fn (design-fix x)
                                 moddb aliases)
         (svex-design-flatten-fn x moddb aliases)))

Theorem: svex-design-flatten-fn-design-equiv-congruence-on-x

(defthm svex-design-flatten-fn-design-equiv-congruence-on-x
  (implies (design-equiv x x-equiv)
           (equal (svex-design-flatten-fn x moddb aliases)
                  (svex-design-flatten-fn x-equiv moddb aliases)))
  :rule-classes :congruence)

Theorem: svex-design-flatten-fn-of-moddb-fix-moddb

(defthm svex-design-flatten-fn-of-moddb-fix-moddb
  (equal (svex-design-flatten-fn x (moddb-fix moddb)
                                 aliases)
         (svex-design-flatten-fn x moddb aliases)))

Theorem: svex-design-flatten-fn-moddb-equiv-congruence-on-moddb

(defthm svex-design-flatten-fn-moddb-equiv-congruence-on-moddb
  (implies (moddb-equiv moddb moddb-equiv)
           (equal (svex-design-flatten-fn x moddb aliases)
                  (svex-design-flatten-fn x moddb-equiv aliases)))
  :rule-classes :congruence)

Theorem: svex-design-flatten-fn-of-lhslist-fix-aliases

(defthm svex-design-flatten-fn-of-lhslist-fix-aliases
  (equal (svex-design-flatten-fn x moddb (lhslist-fix aliases))
         (svex-design-flatten-fn x moddb aliases)))

Theorem: svex-design-flatten-fn-lhslist-equiv-congruence-on-aliases

(defthm svex-design-flatten-fn-lhslist-equiv-congruence-on-aliases
  (implies (lhslist-equiv aliases aliases-equiv)
           (equal (svex-design-flatten-fn x moddb aliases)
                  (svex-design-flatten-fn x moddb aliases-equiv)))
  :rule-classes :congruence)