• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • 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
        • Assign->netassigns
      • Svmods
      • Svstmt
      • Sv-tutorial
      • Expressions
      • Symbolic-test-vector
      • Vl-to-svex
    • Vwsim
    • Fgl
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Testing-utilities
  • Math

• Svex-compilation

Svex-design-flatten-and-normalize

Flatten a hierarchical SV design and apply alias normalization to it.

Signature

(svex-design-flatten-and-normalize x &key (indexedp 'nil) 
                                   (moddb 'moddb) 
                                   (aliases 'aliases)) 
 
  → 
(mv err flat-assigns flat-delays 
    flat-constraints new-moddb new-aliases) 

Arguments

x — Guard (design-p x).

moddb — overwritten.

aliases — overwritten.

Returns

flat-assigns — Type (svex-alist-p flat-assigns).

flat-delays — Type (svex-alist-p flat-delays).

flat-constraints — Type (constraintlist-p flat-constraints).

new-moddb — Type (and (moddb-basics-ok new-moddb) (moddb-mods-ok new-moddb)).

This does all of the steps of svex-design-compile except for the final composition of local assignments into global 0-delay update functions.

Definitions and Theorems

Function: svex-design-flatten-and-normalize-fn

(defun
 svex-design-flatten-and-normalize-fn
 (x indexedp moddb aliases)
 (declare (xargs :stobjs (moddb aliases)))
 (declare (xargs :guard (design-p x)))
 (declare (xargs :guard (modalist-addr-p (design->modalist x))))
 (let
  ((__function__ 'svex-design-flatten-and-normalize))
  (declare (ignorable __function__))
  (b*
   (((mv err assigns
         fixups constraints moddb aliases)
     (svex-design-flatten x))
    ((when err)
     (mv err nil nil nil moddb aliases))
    (modidx (moddb-modname-get-index (design->top x)
                                     moddb))
    ((mv aliases var-decl-map)
     (if
      indexedp
      (b* ((map (cwtime (aliases-to-var-decl-map
                             aliases
                             (make-modscope-top :modidx modidx)
                             moddb)
                        :mintime 1)))
          (mv aliases map))
      (cwtime
          (aliases-indexed->named aliases
                                  (make-modscope-top :modidx modidx)
                                  moddb)
          :mintime 1)))
    ((mv res-assigns res-delays res-constraints)
     (svex-normalize-assigns assigns fixups
                             constraints var-decl-map aliases)))
   (mv nil res-assigns res-delays
       res-constraints moddb aliases))))

Theorem: svex-alist-p-of-svex-design-flatten-and-normalize.flat-assigns

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

Theorem: svex-alist-p-of-svex-design-flatten-and-normalize.flat-delays

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

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

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

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

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

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

(defthm
 alias-length-of-svex-design-flatten-and-normalize
 (b*
  (((mv ?err ?flat-assigns
        ?flat-delays ?flat-constraints
        ?new-moddb ?new-aliases)
    (svex-design-flatten-and-normalize-fn
         x indexedp 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-and-normalize

(defthm
 modidx-of-svex-design-flatten-and-normalize
 (b* (((mv ?err ?flat-assigns
           ?flat-delays ?flat-constraints
           ?new-moddb ?new-aliases)
       (svex-design-flatten-and-normalize-fn
            x indexedp 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-and-normalize-fn
                              x indexedp moddb aliases)))
            (natp (moddb-modname-get-index
                       (design->top x)
                       (mv-nth 4
                               (svex-design-flatten-and-normalize-fn
                                    x indexedp moddb aliases))))))))

Theorem: vars-of-svex-design-flatten-and-normalize

(defthm
    vars-of-svex-design-flatten-and-normalize
    (b* (((mv ?err ?flat-assigns
              ?flat-delays ?flat-constraints
              ?new-moddb ?new-aliases)
          (svex-design-flatten-and-normalize-fn
               x indexedp moddb aliases)))
        (implies (and (modalist-addr-p (design->modalist x))
                      (not indexedp))
                 (svarlist-addr-p (svex-alist-vars flat-assigns)))))

Theorem: vars-of-svex-design-flatten-and-normalize-delays

(defthm
     vars-of-svex-design-flatten-and-normalize-delays
     (b* (((mv ?err ?flat-assigns
               ?flat-delays ?flat-constraints
               ?new-moddb ?new-aliases)
           (svex-design-flatten-and-normalize-fn
                x indexedp moddb aliases)))
         (implies (and (modalist-addr-p (design->modalist x))
                       (not indexedp))
                  (svarlist-addr-p (svex-alist-vars flat-delays)))))

Theorem: vars-of-svex-design-flatten-and-normalize-delays-keys

(defthm
     vars-of-svex-design-flatten-and-normalize-delays-keys
     (b* (((mv ?err ?flat-assigns
               ?flat-delays ?flat-constraints
               ?new-moddb ?new-aliases)
           (svex-design-flatten-and-normalize-fn
                x indexedp moddb aliases)))
         (implies (and (modalist-addr-p (design->modalist x))
                       (not indexedp))
                  (svarlist-addr-p (svex-alist-keys flat-delays)))))

Theorem: vars-of-svex-design-flatten-and-normalize-constraints

(defthm
 vars-of-svex-design-flatten-and-normalize-constraints
 (b*
    (((mv ?err ?flat-assigns
          ?flat-delays ?flat-constraints
          ?new-moddb ?new-aliases)
      (svex-design-flatten-and-normalize-fn
           x indexedp moddb aliases)))
    (implies
         (and (modalist-addr-p (design->modalist x))
              (not indexedp))
         (svarlist-addr-p (constraintlist-vars flat-constraints)))))

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

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

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

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

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

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

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

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

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

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

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

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

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

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