• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
      • Svex-stvs
      • Svex-decomposition-methodology
      • Sv-versus-esim
      • Svex-decomp
      • Svex-compose-dfs
      • Svex-compilation
        • Alias-normalization
        • Svex-design-flatten-and-normalize
        • Svex-design-compile
        • Svex-composition
        • Compile.lisp
        • Assign->segment-drivers
        • Segment-driver-map-resolve
        • Assigns->segment-drivers
      • Moddb
      • Svmods
      • Svstmt
      • Sv-tutorial
      • Expressions
      • Symbolic-test-vector
      • Vl-to-svex
    • Vwsim
    • Fgl
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

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