• 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
            • Svex-normalize-assigns
            • Svex-design-flatten
            • Svex-override-lhrange
            • Svex-override-lhs
            • Aliases-indexed->named-aux
            • Svex-compose-assigns/delays
            • 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
            • Svar-register-indnamememo
            • Svarlist-indexed->named
            • Maybe-svar-fix
            • Lhs-register-indnamememo
            • Maybe-indname-result
            • Aliases-to-var-decl-map
            • Svar-indexed->named
            • Aliases-boundedp-aux
            • Svex-apply-overrides
            • Indnamememo-to-var-decl-map
            • Indname-result
            • Assigns-compose
            • Delay-svarlist->delays
            • Indnamememo
            • Svex-override-vars
            • Delay-svar->delays
            • Assigns-to-overrides
            • Svarlist-collect-delays
            • Svex-overridelist-vars
            • Svex-overridelist-keys
            • Assigns-to-overrides-nrev
            • Var-decl-map
            • Cap-length
          • Assign->segment-drivers
          • Segment-driver-map-resolve
          • Assigns->segment-drivers
        • Moddb
        • Svmods
        • Svstmt
        • Sv-tutorial
        • Expressions
        • Symbolic-test-vector
        • Vl-to-svex
      • Fgl
      • Vwsim
      • Vl
      • X86isa
      • Svl
      • Rtl
    • Software-verification
    • Math
    • Testing-utilities
  • Svex-compilation

Compile.lisp

Subtopics

Svex-normalize-assigns
Svex-design-flatten
Svex-override-lhrange
Svex-override-lhs
Aliases-indexed->named-aux
Svex-compose-assigns/delays
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
Svar-register-indnamememo
Svarlist-indexed->named
Maybe-svar-fix
Lhs-register-indnamememo
Maybe-indname-result
Option type; indname-result or nil.
Aliases-to-var-decl-map
Svar-indexed->named
Aliases-boundedp-aux
Svex-apply-overrides
Indnamememo-to-var-decl-map
Indname-result
Assigns-compose
Delay-svarlist->delays
Indnamememo
Abstract stobj: logically this just represents a list of |SV|::|MAYBE-INDNAME-RESULT-P|s, but it is implemented as an array.
Svex-override-vars
Delay-svar->delays
Assigns-to-overrides
Svarlist-collect-delays
Svex-overridelist-vars
Svex-overridelist-keys
Assigns-to-overrides-nrev
Var-decl-map
An alist mapping svar-p to wire-p.
Cap-length