• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
    • Vwsim
    • Fgl
    • Vl
      • Syntax
      • Loader
      • Warnings
      • Getting-started
      • Utilities
      • Printer
      • Kit
      • Mlib
        • Scopestack
        • Hid-tools
        • Filtering-by-name
        • Vl-interface-mocktype
        • Stripping-functions
        • Genblob
        • Expr-tools
        • Extract-vl-types
        • Hierarchy
        • Range-tools
        • Finding-by-name
        • Stmt-tools
        • Modnamespace
        • Flat-warnings
        • Reordering-by-name
        • Datatype-tools
        • Syscalls
          • Vl-syscall->returninfo
          • Vl-unary-syscall-p
          • Vl-typearg-syscall-p
          • Vl-0ary-syscall-p
          • Vl-*ary-syscall-p
          • Vl-$random-expr-p
          • Vl-simple-id-name
          • Vl-unary-syscall->arg
        • Allexprs
        • Lvalues
        • Port-tools
      • Transforms
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Syscalls

Vl-syscall->returninfo

(Attempt to) look up the return type of a system function call.

Signature

(vl-syscall->returninfo x) → info

Arguments

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

Returns

info — Information about the return type for this system call, if available.
    Type (iff (vl-coredatatype-info-p info) info).

Some system calls don't necessarily have a well-defined or sensible return type, for instance, what is the return type of $finish? So, in some cases we will return nil.

Even if certain system calls don't make sense in the context of synthesis, it is generally useful (e.g., for linting) to be able to look up their return types. So, it would be good to extend this function to make it more complete.

Definitions and Theorems

Function: vl-syscall->returninfo

(defun vl-syscall->returninfo (x)
  (declare (xargs :guard (vl-expr-p x)))
  (declare (xargs :guard (vl-expr-case x
                                       :vl-call x.systemp
                                       :otherwise nil)))
  (let ((__function__ 'vl-syscall->returninfo))
    (declare (ignorable __function__))
    (cond ((vl-0ary-syscall-p "$time" x)
           '((:vl-time :vl-kwd-time) (t) t . 64))
          ((or (vl-unary-syscall-p "$bits" x)
               (vl-typearg-syscall-p "$bits" x))
           '((:vl-integer :vl-kwd-integer . t)
             (t)
             t . 32))
          ((or (vl-*ary-syscall-p "$left" x)
               (vl-*ary-syscall-p "$right" x)
               (vl-*ary-syscall-p "$low" x)
               (vl-*ary-syscall-p "$high" x)
               (vl-*ary-syscall-p "$increment" x)
               (vl-*ary-syscall-p "$size" x))
           '((:vl-integer :vl-kwd-integer . t)
             (t)
             t . 32))
          ((or (vl-unary-syscall-p "$dimensions" x)
               (vl-unary-syscall-p "$unpacked_dimensions" x))
           '((:vl-integer :vl-kwd-integer . t)
             (t)
             t . 32))
          ((vl-unary-syscall-p "$clog2" x)
           '((:vl-integer :vl-kwd-integer . t)
             (t)
             t . 32))
          ((or (vl-unary-syscall-p "$ln" x)
               (vl-unary-syscall-p "$log10" x))
           '((:vl-real :vl-kwd-real)))
          ((or (vl-*ary-syscall-p "$countbits" x)
               (vl-unary-syscall-p "$countones" x))
           '((:vl-int :vl-kwd-int . t)
             (t)
             nil . 32))
          ((or (vl-unary-syscall-p "$onehot" x)
               (vl-unary-syscall-p "$onehot0" x)
               (vl-unary-syscall-p "$isunknown" x))
           '((:vl-bit :vl-kwd-bit) (t . t) nil . 1))
          ((vl-$random-expr-p x)
           '((:vl-integer :vl-kwd-integer . t)
             (t)
             t . 32))
          ((vl-unary-syscall-p "$test$plusargs" x)
           '((:vl-integer :vl-kwd-integer . t)
             (t)
             t . 32))
          (t nil))))

Theorem: return-type-of-vl-syscall->returninfo

(defthm return-type-of-vl-syscall->returninfo
  (b* ((info (vl-syscall->returninfo x)))
    (iff (vl-coredatatype-info-p info)
         info))
  :rule-classes :rewrite)

Theorem: vl-syscall->returninfo-of-vl-expr-fix-x

(defthm vl-syscall->returninfo-of-vl-expr-fix-x
  (equal (vl-syscall->returninfo (vl-expr-fix x))
         (vl-syscall->returninfo x)))

Theorem: vl-syscall->returninfo-vl-expr-equiv-congruence-on-x

(defthm vl-syscall->returninfo-vl-expr-equiv-congruence-on-x
  (implies (vl-expr-equiv x x-equiv)
           (equal (vl-syscall->returninfo x)
                  (vl-syscall->returninfo x-equiv)))
  :rule-classes :congruence)