• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
      • Svex-stvs
      • Svex-fixpoint-decomposition-methodology
      • Sv-versus-esim
      • Svex-decomp
      • Svex-compose-dfs
      • Moddb
      • Svex-compilation
        • Alias-normalization
        • Svex-design-flatten-and-normalize
        • Svex-design-compile
        • Svex-composition
        • Compile.lisp
          • Svex-normalize-assigns
          • Svex-design-flatten
          • Svex-override-lhrange
          • Svex-override-lhs
          • Svex-compose-assigns/delays
          • Aliases-indexed->named-aux
          • Svex-alist-truncate-by-var-decls
          • Svar-map-truncate-by-var-decls
          • Aliases-to-var-decl-map-aux
          • Aliases-indexed->named
          • Svar-indexed->named-memo
          • Lhs-indexed->named
          • Maybe-svar-p
          • Svar-register-indnamememo
          • Svarlist-indexed->named
          • Maybe-svar-fix
          • Lhs-register-indnamememo
          • Maybe-indname-result
          • Aliases-to-var-decl-map
          • Svar-indexed->named
          • Svex-apply-overrides
          • Aliases-boundedp-aux
          • Indnamememo-to-var-decl-map
          • Indname-result
          • Assigns-compose
          • Delay-svarlist->delays
          • Svex-override-vars
          • Indnamememo
          • Delay-svar->delays
          • Assigns-to-overrides
          • Svarlist-collect-delays
          • Svex-overridelist-vars
          • Svex-overridelist-keys
          • Assigns-to-overrides-nrev
          • Cap-length
          • Var-decl-map
        • Assign->netassigns
      • Svmods
      • Svstmt
      • Sv-tutorial
      • Expressions
      • Symbolic-test-vector
      • Vl-to-svex
    • Fgl
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Testing-utilities
  • Math

• 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)