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