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

Compile a hierarchical SVEX design into a finite state machine.

Signature

(svex-design-compile x &key (indexedp 'nil) 
                     (moddb 'moddb) 
                     (aliases 'aliases) 
                     (rewrite 't) 
                     (verbosep 'nil)) 
 
  → 
(mv err composed-updates 
    state-updates composed-constraints 
    flat-assigns flat-delays 
    flat-constraints new-moddb new-aliases) 

Arguments

x — Guard (design-p x).

moddb — overwritten.

aliases — overwritten.

Returns

composed-updates — Type (svex-alist-p composed-updates).

state-updates — Type (svex-alist-p state-updates).

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

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

Definitions and Theorems

Function: svex-design-compile-fn

(defun svex-design-compile-fn
       (x indexedp moddb aliases rewrite verbosep)
  (declare (xargs :stobjs (moddb aliases)))
  (declare (xargs :guard (design-p x)))
  (declare (xargs :guard (modalist-addr-p (design->modalist x))))
  (let ((__function__ 'svex-design-compile))
    (declare (ignorable __function__))
    (b* (((mv err res-assigns res-delays
              res-constraints moddb aliases)
          (svex-design-flatten-and-normalize x
                                             :indexedp indexedp))
         ((mv updates nextstates full-constraints)
          (svex-compose-assigns/delays
               res-assigns res-delays res-constraints
               :rewrite rewrite
               :verbosep verbosep)))
      (mv err updates nextstates
          full-constraints res-assigns res-delays
          res-constraints moddb aliases))))

Theorem: svex-alist-p-of-svex-design-compile.composed-updates

(defthm svex-alist-p-of-svex-design-compile.composed-updates
  (b* (((mv ?err ?composed-updates ?state-updates
            ?composed-constraints ?flat-assigns
            ?flat-delays ?flat-constraints
            ?new-moddb ?new-aliases)
        (svex-design-compile-fn x indexedp
                                moddb aliases rewrite verbosep)))
    (svex-alist-p composed-updates))
  :rule-classes :rewrite)

Theorem: svex-alist-p-of-svex-design-compile.state-updates

(defthm svex-alist-p-of-svex-design-compile.state-updates
  (b* (((mv ?err ?composed-updates ?state-updates
            ?composed-constraints ?flat-assigns
            ?flat-delays ?flat-constraints
            ?new-moddb ?new-aliases)
        (svex-design-compile-fn x indexedp
                                moddb aliases rewrite verbosep)))
    (svex-alist-p state-updates))
  :rule-classes :rewrite)

Theorem: constraintlist-p-of-svex-design-compile.composed-constraints

(defthm constraintlist-p-of-svex-design-compile.composed-constraints
  (b* (((mv ?err ?composed-updates ?state-updates
            ?composed-constraints ?flat-assigns
            ?flat-delays ?flat-constraints
            ?new-moddb ?new-aliases)
        (svex-design-compile-fn x indexedp
                                moddb aliases rewrite verbosep)))
    (constraintlist-p composed-constraints))
  :rule-classes :rewrite)

Theorem: svex-alist-p-of-svex-design-compile.flat-assigns

(defthm svex-alist-p-of-svex-design-compile.flat-assigns
  (b* (((mv ?err ?composed-updates ?state-updates
            ?composed-constraints ?flat-assigns
            ?flat-delays ?flat-constraints
            ?new-moddb ?new-aliases)
        (svex-design-compile-fn x indexedp
                                moddb aliases rewrite verbosep)))
    (svex-alist-p flat-assigns))
  :rule-classes :rewrite)

Theorem: svex-alist-p-of-svex-design-compile.flat-delays

(defthm svex-alist-p-of-svex-design-compile.flat-delays
  (b* (((mv ?err ?composed-updates ?state-updates
            ?composed-constraints ?flat-assigns
            ?flat-delays ?flat-constraints
            ?new-moddb ?new-aliases)
        (svex-design-compile-fn x indexedp
                                moddb aliases rewrite verbosep)))
    (svex-alist-p flat-delays))
  :rule-classes :rewrite)

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

(defthm constraintlist-p-of-svex-design-compile.flat-constraints
  (b* (((mv ?err ?composed-updates ?state-updates
            ?composed-constraints ?flat-assigns
            ?flat-delays ?flat-constraints
            ?new-moddb ?new-aliases)
        (svex-design-compile-fn x indexedp
                                moddb aliases rewrite verbosep)))
    (constraintlist-p flat-constraints))
  :rule-classes :rewrite)

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

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

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

(defthm alias-length-of-svex-design-compile
 (b* (((mv ?err ?composed-updates ?state-updates
           ?composed-constraints ?flat-assigns
           ?flat-delays ?flat-constraints
           ?new-moddb ?new-aliases)
       (svex-design-compile-fn x indexedp
                               moddb aliases rewrite verbosep)))
  (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-compile

(defthm modidx-of-svex-design-compile
 (b* (((mv ?err ?composed-updates ?state-updates
           ?composed-constraints ?flat-assigns
           ?flat-delays ?flat-constraints
           ?new-moddb ?new-aliases)
       (svex-design-compile-fn x indexedp
                               moddb aliases rewrite verbosep)))
   (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-compile-fn x indexedp
                                   moddb aliases rewrite verbosep)))
    (natp (moddb-modname-get-index
               (design->top x)
               (mv-nth 7
                       (svex-design-compile-fn
                            x indexedp
                            moddb aliases rewrite verbosep))))))))

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

(defthm svex-design-compile-fn-of-design-fix-x
 (equal
    (svex-design-compile-fn (design-fix x)
                            indexedp moddb aliases rewrite verbosep)
    (svex-design-compile-fn x indexedp
                            moddb aliases rewrite verbosep)))

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

(defthm svex-design-compile-fn-design-equiv-congruence-on-x
 (implies
  (design-equiv x x-equiv)
  (equal
    (svex-design-compile-fn x
                            indexedp moddb aliases rewrite verbosep)
    (svex-design-compile-fn x-equiv indexedp
                            moddb aliases rewrite verbosep)))
 :rule-classes :congruence)

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

(defthm svex-design-compile-fn-of-moddb-fix-moddb
  (equal (svex-design-compile-fn x indexedp (moddb-fix moddb)
                                 aliases rewrite verbosep)
         (svex-design-compile-fn x indexedp
                                 moddb aliases rewrite verbosep)))

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

(defthm svex-design-compile-fn-moddb-equiv-congruence-on-moddb
 (implies
  (moddb-equiv moddb moddb-equiv)
  (equal
    (svex-design-compile-fn x
                            indexedp moddb aliases rewrite verbosep)
    (svex-design-compile-fn x indexedp
                            moddb-equiv aliases rewrite verbosep)))
 :rule-classes :congruence)

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

(defthm svex-design-compile-fn-of-lhslist-fix-aliases
 (equal
      (svex-design-compile-fn x indexedp moddb (lhslist-fix aliases)
                              rewrite verbosep)
      (svex-design-compile-fn x indexedp
                              moddb aliases rewrite verbosep)))

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

(defthm svex-design-compile-fn-lhslist-equiv-congruence-on-aliases
 (implies
  (lhslist-equiv aliases aliases-equiv)
  (equal
    (svex-design-compile-fn x
                            indexedp moddb aliases rewrite verbosep)
    (svex-design-compile-fn x indexedp
                            moddb aliases-equiv rewrite verbosep)))
 :rule-classes :congruence)