• 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
      • Moddb
      • Svmods
      • Svstmt
      • Sv-tutorial
      • Expressions
      • Symbolic-test-vector
      • Vl-to-svex
        • Vl-to-sv
        • Vl-design->sv-design
          • Vl-simpconfig
          • Vl-hierarchy-sv-translation
          • Vl-expr-svex-translation
            • Sv::vl-expr.lisp
              • Vl-scopecontext-to-addr
              • Vl-binaryop-to-svex
              • Vl-expr-to-svex-maybe-typed
              • Vl-datatype-syscall-to-svex
              • Vl-operandinfo-to-svex-preproc
              • Vl-structmemberlist->types
              • Vl-seltrace-to-svex-select
              • Vl-portdecllist->types
              • Vl-operandinfo-to-svex-select
              • Vl-plusminus-partselect->svex
              • Vl-arrayrange->rel-lsb-and-width
              • Vl-unaryop-to-svex
              • Vl-funcall-args-to-ordered
              • Vl-expr-to-svex-lhs
              • Vl-operandinfo-to-svex
              • Vl-array-assignpat-keyval-resolve
              • Vl-err->vfatal
              • Vl-datatypelist-usertype-resolve
              • Vl-upscope-to-svex-upscope
              • Vl-err->fatal
              • Vl-streaming-concat-trunc/extend
              • Vl-operandinfo-base-svar
              • Vl-index-shift-amount
              • Vttree->constraints
              • Vl-slicesize-resolve
              • Vl-function-map-find-matching-aux
              • Vl-funname-lookup
              • Vl-datatype-size-warn
              • Svex-repeat-aux
              • Vl-$test$plusargs-to-svex
              • Svex-extend
              • Vl-structmemberlist-shift-bits
              • Vl-datatype-slot-width/range
              • Vl-datatype-index-shift-amount
              • Vl-datatype-field-shift-amount
              • 4vec-extend
              • Vl-function-pair-inputs-with-actuals
              • Vl-expr-to-svex-untyped
              • Vl-function-map-check-matching
              • Vl-datatype-syscall-remove-dims
              • Svex-concat-list-aux
              • Vttree-add-constraints
              • Vttree-add-warnings
              • Vl-check-struct-assignpat-keys
              • Vl-check-array-assignpat-keys
              • Sv::constraintlist-subst-memo
              • Vl-svex-keyval-index-lookup
              • Vl-function-map-find-matching
              • Vl-convert-dollarsign-to-expr
              • Vttree->constraints-acc
              • Vl-seltrace-type
              • Vl-seltrace-to-path
              • Vl-keyval-member-lookup
              • Svex-repeat
              • Vttree->warnings-acc
              • Vl-trunc/extend-type-err
              • Constraintlist-add-ctx
              • Vl-hidtrace-add-to-path
              • Svex-multiconcat
              • Vttree-join
              • Vl-value-to-string-aux
              • Vl-seltrace-add-to-path
              • Vl-value-to-4vec
              • Vl-expr-to-svex-selfdet
              • Vl-svex-keyval-default-lookup
              • Vl-$test$plusargs-p
              • Vl-value-to-svex
              • Vl-value-in-range
              • Vl-keyval-default-lookup
              • Sv::svexlist-args-extract-constants
              • Vl-string->bits
              • Vl-size-to-unsigned-logic
              • Vl-hidtrace-to-path
              • Svex-concat-list
              • Vttree->warnings
              • Vl-seltrace-unres-count
              • Vl-datatype-index-is-bitselect
              • Vl-bitlist->4vec
              • Vl-svex-keyvallist-vars
              • Vl-hidstep->svex-index
              • Vl-selstep->svex-name
              • Vl-datatypelist-resolved-p
              • Vl-datatype-$unpacked_dimensions
              • Vl-datatype-$dimensions
              • Vl-bitlist->offset
              • Vl-bitlist->onset
              • Vl-streamexprlist-has-with
              • Vl-hidstep-resolved-p
              • Vl-expr-needs-type-context
              • Vl-streamexprlist->exprs
              • Vl-integer-to-string
              • Vl-hidtrace-resolved-p
              • Vl-selstep-resolved-p
              • Vl-select-resolved-p
              • Vl-svex-keyvallist
              • Vl-datatypelist
              • Svex-x
            • Vttree
          • Vl-design->svex-modalist
          • Vl-svstmt
        • Vl-to-sv-main
        • Vl-simplify-sv
        • Vl-user-paramsettings->unparam-names
        • Vl-user-paramsettings->modnames
    • Vwsim
    • Fgl
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Sv::vl-expr.lisp

Vl-datatype-syscall-to-svex

Signature

(vl-datatype-syscall-to-svex orig-x fn type index ss scopes) 
  → 
(mv warnings res)

Arguments

orig-x — Guard (vl-expr-p orig-x).

fn — Guard (stringp fn).

type — Guard (vl-datatype-p type).

index — Guard (maybe-natp index).

ss — Guard (vl-scopestack-p ss).

scopes — Guard (vl-elabscopes-p scopes).

Returns

warnings — Type (vl-warninglist-p warnings).

res — Type (sv::svex-p res).

Definitions and Theorems

Function: vl-datatype-syscall-to-svex

(defun vl-datatype-syscall-to-svex (orig-x fn type index ss scopes)
 (declare (xargs :guard (and (vl-expr-p orig-x)
                             (stringp fn)
                             (vl-datatype-p type)
                             (maybe-natp index)
                             (vl-scopestack-p ss)
                             (vl-elabscopes-p scopes))))
 (let ((__function__ 'vl-datatype-syscall-to-svex))
  (declare (ignorable __function__))
  (b*
   ((warnings nil)
    (fn (string-fix fn))
    (index (maybe-natp-fix index))
    (orig-x (vl-expr-fix orig-x))
    ((when (and index (zp index)))
     (mv
      (fatal
       :type :vl-expr-to-svex-fail
       :msg
       "Dimension argument of 0 is illegal in array query system calls: ~a0"
       :args (list orig-x))
      (svex-x)))
    ((when
        (and index
             (member-equal
                  fn
                  '("$bits" "$dimensions" "$unpacked_dimensions"))))
     (mv (fatal :type :vl-expr-to-svex-fail
                :msg "Dimension argument is illegal: ~a0"
                :args (list orig-x))
         (svex-x)))
    ((mv err type)
     (vl-datatype-usertype-resolve type ss
                                   :scopes scopes))
    ((when err)
     (mv (fatal :type :vl-expr-to-svex-fail
                :msg "Couldn't resolve datatype in ~a0: ~@1"
                :args (list orig-x err))
         (svex-x))))
   (cond
    ((equal fn "$bits")
     (b*
      (((mv err size) (vl-datatype-size type))
       ((when (or err (not size)))
        (mv
           (fatal :type :vl-expr-to-svex-fail
                  :msg "Couldn't size datatype in ~a0: ~@1"
                  :args (list orig-x (or err "unsizable datatype")))
           (svex-x))))
      (mv (ok) (svex-int size))))
    ((equal fn "$dimensions")
     (mv nil
         (svex-int (vl-datatype-$dimensions type))))
    ((equal fn "$unpacked_dimensions")
     (mv nil
         (svex-int (vl-datatype-$unpacked_dimensions type))))
    ((member-equal fn
                   '("$left" "$right"
                             "$increment" "$low" "$high" "$size"))
     (b*
      (((mv err dim)
        (vl-datatype-syscall-remove-dims (if index (1- index) 0)
                                         type))
       ((when
         (or err (not (vl-dimension-case dim :range))
             (not (vl-range-resolved-p (vl-dimension->range dim)))))
        (mv
         (fatal
            :type :vl-expr-to-svex-fail
            :msg "Couldn't resolve outermost dimension for ~a0: ~@1"
            :args (list orig-x (or err "unresolved dimension")))
         (svex-x)))
       (dim.range (vl-dimension->range dim))
       ((vl-range dim) dim.range))
      (cond ((equal fn "$left")
             (mv nil
                 (svex-int (vl-resolved->val dim.msb))))
            ((equal fn "$right")
             (mv nil
                 (svex-int (vl-resolved->val dim.lsb))))
            ((equal fn "$increment")
             (mv nil
                 (svex-int (if (< (vl-resolved->val dim.msb)
                                  (vl-resolved->val dim.lsb))
                               -1
                             1))))
            ((equal fn "$low")
             (mv nil
                 (svex-int (if (< (vl-resolved->val dim.msb)
                                  (vl-resolved->val dim.lsb))
                               (vl-resolved->val dim.msb)
                             (vl-resolved->val dim.lsb)))))
            ((equal fn "$high")
             (mv nil
                 (svex-int (if (< (vl-resolved->val dim.msb)
                                  (vl-resolved->val dim.lsb))
                               (vl-resolved->val dim.lsb)
                             (vl-resolved->val dim.msb)))))
            (t (mv nil
                   (svex-int (vl-range-size dim.range)))))))
    (t (mv (fatal :type :vl-expr-unsupported
                  :msg "Unrecognized system function: ~a0"
                  :args (list orig-x))
           (svex-x)))))))

Theorem: vl-warninglist-p-of-vl-datatype-syscall-to-svex.warnings

(defthm vl-warninglist-p-of-vl-datatype-syscall-to-svex.warnings
  (b*
    (((mv ?warnings ?res)
      (vl-datatype-syscall-to-svex orig-x fn type index ss scopes)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)

Theorem: svex-p-of-vl-datatype-syscall-to-svex.res

(defthm svex-p-of-vl-datatype-syscall-to-svex.res
  (b*
    (((mv ?warnings ?res)
      (vl-datatype-syscall-to-svex orig-x fn type index ss scopes)))
    (sv::svex-p res))
  :rule-classes :rewrite)

Theorem: vars-of-vl-datatype-syscall-to-svex

(defthm vars-of-vl-datatype-syscall-to-svex
  (b*
    (((mv ?warnings ?res)
      (vl-datatype-syscall-to-svex orig-x fn type index ss scopes)))
    (equal (sv::svex-vars res) nil)))

Theorem: vl-datatype-syscall-to-svex-of-vl-expr-fix-orig-x

(defthm vl-datatype-syscall-to-svex-of-vl-expr-fix-orig-x
 (equal
      (vl-datatype-syscall-to-svex (vl-expr-fix orig-x)
                                   fn type index ss scopes)
      (vl-datatype-syscall-to-svex orig-x fn type index ss scopes)))

Theorem: vl-datatype-syscall-to-svex-vl-expr-equiv-congruence-on-orig-x

(defthm
     vl-datatype-syscall-to-svex-vl-expr-equiv-congruence-on-orig-x
 (implies
   (vl-expr-equiv orig-x orig-x-equiv)
   (equal
        (vl-datatype-syscall-to-svex orig-x fn type index ss scopes)
        (vl-datatype-syscall-to-svex
             orig-x-equiv fn type index ss scopes)))
 :rule-classes :congruence)

Theorem: vl-datatype-syscall-to-svex-of-str-fix-fn

(defthm vl-datatype-syscall-to-svex-of-str-fix-fn
 (equal
      (vl-datatype-syscall-to-svex orig-x (str-fix fn)
                                   type index ss scopes)
      (vl-datatype-syscall-to-svex orig-x fn type index ss scopes)))

Theorem: vl-datatype-syscall-to-svex-streqv-congruence-on-fn

(defthm vl-datatype-syscall-to-svex-streqv-congruence-on-fn
 (implies
   (streqv fn fn-equiv)
   (equal
        (vl-datatype-syscall-to-svex orig-x fn type index ss scopes)
        (vl-datatype-syscall-to-svex
             orig-x fn-equiv type index ss scopes)))
 :rule-classes :congruence)

Theorem: vl-datatype-syscall-to-svex-of-vl-datatype-fix-type

(defthm vl-datatype-syscall-to-svex-of-vl-datatype-fix-type
 (equal
      (vl-datatype-syscall-to-svex orig-x fn (vl-datatype-fix type)
                                   index ss scopes)
      (vl-datatype-syscall-to-svex orig-x fn type index ss scopes)))

Theorem: vl-datatype-syscall-to-svex-vl-datatype-equiv-congruence-on-type

(defthm
   vl-datatype-syscall-to-svex-vl-datatype-equiv-congruence-on-type
 (implies
   (vl-datatype-equiv type type-equiv)
   (equal
        (vl-datatype-syscall-to-svex orig-x fn type index ss scopes)
        (vl-datatype-syscall-to-svex
             orig-x fn type-equiv index ss scopes)))
 :rule-classes :congruence)

Theorem: vl-datatype-syscall-to-svex-of-maybe-natp-fix-index

(defthm vl-datatype-syscall-to-svex-of-maybe-natp-fix-index
 (equal
  (vl-datatype-syscall-to-svex orig-x fn type (maybe-natp-fix index)
                               ss scopes)
  (vl-datatype-syscall-to-svex orig-x fn type index ss scopes)))

Theorem: vl-datatype-syscall-to-svex-maybe-nat-equiv-congruence-on-index

(defthm
    vl-datatype-syscall-to-svex-maybe-nat-equiv-congruence-on-index
 (implies
   (acl2::maybe-nat-equiv index index-equiv)
   (equal
        (vl-datatype-syscall-to-svex orig-x fn type index ss scopes)
        (vl-datatype-syscall-to-svex
             orig-x fn type index-equiv ss scopes)))
 :rule-classes :congruence)

Theorem: vl-datatype-syscall-to-svex-of-vl-scopestack-fix-ss

(defthm vl-datatype-syscall-to-svex-of-vl-scopestack-fix-ss
 (equal
   (vl-datatype-syscall-to-svex orig-x
                                fn type index (vl-scopestack-fix ss)
                                scopes)
   (vl-datatype-syscall-to-svex orig-x fn type index ss scopes)))

Theorem: vl-datatype-syscall-to-svex-vl-scopestack-equiv-congruence-on-ss

(defthm
   vl-datatype-syscall-to-svex-vl-scopestack-equiv-congruence-on-ss
 (implies
   (vl-scopestack-equiv ss ss-equiv)
   (equal
        (vl-datatype-syscall-to-svex orig-x fn type index ss scopes)
        (vl-datatype-syscall-to-svex
             orig-x fn type index ss-equiv scopes)))
 :rule-classes :congruence)

Theorem: vl-datatype-syscall-to-svex-of-vl-elabscopes-fix-scopes

(defthm vl-datatype-syscall-to-svex-of-vl-elabscopes-fix-scopes
 (equal
   (vl-datatype-syscall-to-svex orig-x fn type
                                index ss (vl-elabscopes-fix scopes))
   (vl-datatype-syscall-to-svex orig-x fn type index ss scopes)))

Theorem: vl-datatype-syscall-to-svex-vl-elabscopes-equiv-congruence-on-scopes

(defthm
 vl-datatype-syscall-to-svex-vl-elabscopes-equiv-congruence-on-scopes
 (implies
   (vl-elabscopes-equiv scopes scopes-equiv)
   (equal
        (vl-datatype-syscall-to-svex orig-x fn type index ss scopes)
        (vl-datatype-syscall-to-svex
             orig-x fn type index ss scopes-equiv)))
 :rule-classes :congruence)