• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
      • Vl2014
      • Sv
      • Fgl
      • Vwsim
      • Vl
        • Syntax
        • Loader
        • Warnings
        • Getting-started
        • Utilities
        • Printer
          • Ps
          • Verilog-printing
          • Basic-printing
          • Printing-locally
          • Formatted-printing
          • Accessing-printed-output
          • Json-printing
            • Json-encoders
              • Vl-jp-expr
              • Vl-jp-module
              • Vl-jp-interface
              • Vl-jp-design
              • Vl-jp-warning
              • Vl-jp-package
              • Vl-jp-vardecl
              • Vl-jp-class
              • Vl-jp-ansi-portdecl
              • Vl-jp-constint
              • Jp-sym-main
              • Vl-jp-udp
              • Vl-jp-taskdecl
              • Vl-jp-fundecl
              • Vl-jp-clkdecl
              • Vl-jp-modinst
              • Vl-jp-gateinst
              • Vl-jp-dpiimport
              • Vl-jp-typedef
              • Vl-jp-propport
              • Vl-jp-program
              • Vl-jp-portdecl
              • Vl-jp-paramdecl
              • Vl-jp-modport-port
              • Vl-jp-interfaceport
              • Vl-jp-dpiexport
              • Vl-jp-config
              • Vl-jp-assign
              • Jp-str
              • Vl-jp-warninglist
              • Vl-jp-vardecllist
              • Vl-jp-udpentrylist
              • Vl-jp-typedeflist
              • Vl-jp-taskdecllist
              • Vl-jp-sequencelist
              • Vl-jp-sequence
              • Vl-jp-propportlist
              • Vl-jp-propertylist
              • Vl-jp-property
              • Vl-jp-programlist
              • Vl-jp-portdecllist
              • Vl-jp-plainarglist
              • Vl-jp-parse-temps
              • Vl-jp-paramvaluelist
              • Vl-jp-paramdecllist
              • Vl-jp-packagelist
              • Vl-jp-namedparamvaluelist
              • Vl-jp-namedarglist
              • Vl-jp-modportlist
              • Vl-jp-modport-portlist
              • Vl-jp-modinstlist
              • Vl-jp-locationlist
              • Vl-jp-interfacelist
              • Vl-jp-initiallist
              • Vl-jp-gclkdecllist
              • Vl-jp-gateinstlist
              • Vl-jp-fwdtypedeflist
              • Vl-jp-fwdtypedef
              • Vl-jp-fundecllist
              • Vl-jp-exprdistlist
              • Vl-jp-elabtasklist
              • Vl-jp-dpiimportlist
              • Vl-jp-dpiexportlist
              • Vl-jp-defaultdisablelist
              • Vl-jp-covergrouplist
              • Vl-jp-clkdecllist
              • Vl-jp-clkassignlist
              • Vl-jp-clkassign
              • Vl-jp-cassertionlist
              • Vl-jp-blockitemlist
              • Vl-jp-bind
              • Vl-jp-assertionlist
              • Vl-jp-ansi-portdecllist
              • Jp-nat
              • Vl-jp-udplist
              • Vl-jp-udplinelist
              • Vl-jp-udpline
              • Vl-jp-timeunitdecl
              • Vl-jp-timeprecisiondecl
              • Vl-jp-repetition
              • Vl-jp-repeateventcontrol
              • Vl-jp-regularport
              • Vl-jp-propspec
              • Vl-jp-portlist
              • Vl-jp-plainarg
              • Vl-jp-namedparamvalue
              • Vl-jp-namedarg
              • Vl-jp-modulelist
              • Vl-jp-modport
              • Vl-jp-initial
              • Vl-jp-importlist
              • Vl-jp-import
              • Vl-jp-genvarlist
              • Vl-jp-gclkdecl
              • Vl-jp-gatestrength
              • Vl-jp-gatedelay
              • Vl-jp-finallist
              • Vl-jp-eventcontrol
              • Vl-jp-distitemlist
              • Vl-jp-distitem
              • Vl-jp-defaultdisable
              • Vl-jp-covergroup
              • Vl-jp-configlist
              • Vl-jp-classlist
              • Vl-jp-bindlist
              • Vl-jp-assignlist
              • Vl-jp-alwayslist
              • Vl-jp-always
              • Vl-jp-aliaslist
              • Vl-jp-alias
              • Jp-object
              • Vl-jp-udpedge
              • Vl-jp-timeliteral
              • Vl-jp-maybe-timeunitdecl
              • Vl-jp-maybe-timeprecisiondecl
              • Vl-jp-maybe-gatestrength
              • Vl-jp-maybe-delayoreventcontrol
              • Vl-jp-genvar
              • Vl-jp-final
              • Vl-jp-exprdist
              • Vl-jp-delaycontrol
              • Vl-jp-clkskew
              • Vl-jp-maybe-udpsymbol
              • Vl-jp-maybe-timeliteral
              • Vl-jp-maybe-scopeid
              • Vl-jp-maybe-rhs
              • Vl-jp-maybe-parse-temps
              • Vl-jp-maybe-paramvalue
              • Vl-jp-maybe-nettypename
              • Vl-jp-maybe-module
              • Vl-jp-maybe-gatedelay
              • Vl-jp-maybe-exprdist
              • Vl-jp-maybe-clkskew
              • Vl-jp-elabtask
              • Vl-jp-weirdint
              • Vl-jp-value
              • Vl-jp-time
              • Vl-jp-string
              • Vl-jp-maybe-direction
              • Vl-jp-maybe-cstrength
              • Vl-jp-extint
              • Jp-timeunit
              • Jp-bool
              • Jp-bitlist
              • Jp-bit
              • Jp-bignat
              • Vl-jp-real
              • Vl-jp-maybe-exprsign
              • Vl-jp-gatetype
              • Vl-jp-exprsign
              • Vl-jp-evatomtype
              • Vl-jp-dstrength
              • Vl-jp-direction
              • Vl-jp-deassign-type
              • Vl-jp-cstrength
              • Vl-jp-casetype
              • Vl-jp-casekey
              • Vl-jp-casecheck
              • Vl-jp-assign-type
              • Vl-jp-alwaystype
              • Jp-maybe-string
              • Jp-maybe-nat
              • Jp-sym
          • Vl-printedlist
        • Kit
        • Mlib
        • Transforms
      • X86isa
      • Svl
      • Rtl
    • Software-verification
    • Math
    • Testing-utilities
  • Json-printing

Json-encoders

A table of JSON encoders to use for for different kinds of data.

A JSON encoder is a function of the following signature:

encode-foo : foo * ps --> ps

Where foo is expected to be an object of some type foop, and ps is the vl printer state stobj, ps. Each such routine is responsible for printing a JSON encoding of its foop argument. Each such function may assume that ps is set to text mode.

The encoder table is a simple association of foop to encode-foo functions. We can use it to automatically generate encoders for, e.g., defaggregate structures.

Definitions and Theorems

Function: get-json-encoders

(defun get-json-encoders (world)
  "Look up the current alist of json encoders."
  (cdr (assoc 'encoders
              (table-alist 'vl-json world))))

Function: get-json-encoder

(defun get-json-encoder (foop world)
  (let ((entry (assoc foop (get-json-encoders world))))
    (if entry (cdr entry)
      (er hard? 'get-json-encoder
          "No json encoder defined for ~x0.~%"
          foop))))

Subtopics

Vl-jp-expr
Vl-jp-module
Print the JSON encoding of a vl-module-p to ps.
Vl-jp-interface
Print the JSON encoding of a vl-interface-p to ps.
Vl-jp-design
Print the JSON encoding of a vl-design-p to ps.
Vl-jp-warning
Special, custom JSON encoder for warnings.
Vl-jp-package
Print the JSON encoding of a vl-package-p to ps.
Vl-jp-vardecl
Print the JSON encoding of a vl-vardecl-p to ps.
Vl-jp-class
Print the JSON encoding of a vl-class-p to ps.
Vl-jp-ansi-portdecl
Print the JSON encoding of a vl-ansi-portdecl-p to ps.
Vl-jp-constint
Jp-sym-main
Encode a simple symbol as a JSON string, including the surrounding quotes.
Vl-jp-udp
Print the JSON encoding of a vl-udp-p to ps.
Vl-jp-taskdecl
Print the JSON encoding of a vl-taskdecl-p to ps.
Vl-jp-fundecl
Print the JSON encoding of a vl-fundecl-p to ps.
Vl-jp-clkdecl
Print the JSON encoding of a vl-clkdecl-p to ps.
Vl-jp-modinst
Print the JSON encoding of a vl-modinst-p to ps.
Vl-jp-gateinst
Print the JSON encoding of a vl-gateinst-p to ps.
Vl-jp-dpiimport
Print the JSON encoding of a vl-dpiimport-p to ps.
Vl-jp-typedef
Print the JSON encoding of a vl-typedef-p to ps.
Vl-jp-propport
Print the JSON encoding of a vl-propport-p to ps.
Vl-jp-program
Print the JSON encoding of a vl-program-p to ps.
Vl-jp-portdecl
Print the JSON encoding of a vl-portdecl-p to ps.
Vl-jp-paramdecl
Print the JSON encoding of a vl-paramdecl-p to ps.
Vl-jp-modport-port
Print the JSON encoding of a vl-modport-port-p to ps.
Vl-jp-interfaceport
Print the JSON encoding of a vl-interfaceport-p to ps.
Vl-jp-dpiexport
Print the JSON encoding of a vl-dpiexport-p to ps.
Vl-jp-config
Print the JSON encoding of a vl-config-p to ps.
Vl-jp-assign
Print the JSON encoding of a vl-assign-p to ps.
Jp-str
Print the JSON encoding of a string, handling all escaping correctly and including the surrounding quotes.
Vl-jp-warninglist
Prints out the elements of a vl-warninglist-p with the enclosing brackets.
Vl-jp-vardecllist
Prints out the elements of a vl-vardecllist-p with the enclosing brackets.
Vl-jp-udpentrylist
Prints out the elements of a vl-udpentrylist-p with the enclosing brackets.
Vl-jp-typedeflist
Prints out the elements of a vl-typedeflist-p with the enclosing brackets.
Vl-jp-taskdecllist
Prints out the elements of a vl-taskdecllist-p with the enclosing brackets.
Vl-jp-sequencelist
Prints out the elements of a vl-sequencelist-p with the enclosing brackets.
Vl-jp-sequence
Print the JSON encoding of a vl-sequence-p to ps.
Vl-jp-propportlist
Prints out the elements of a vl-propportlist-p with the enclosing brackets.
Vl-jp-propertylist
Prints out the elements of a vl-propertylist-p with the enclosing brackets.
Vl-jp-property
Print the JSON encoding of a vl-property-p to ps.
Vl-jp-programlist
Prints out the elements of a vl-programlist-p with the enclosing brackets.
Vl-jp-portdecllist
Prints out the elements of a vl-portdecllist-p with the enclosing brackets.
Vl-jp-plainarglist
Prints out the elements of a vl-plainarglist-p with the enclosing brackets.
Vl-jp-parse-temps
Print the JSON encoding of a vl-parse-temps-p to ps.
Vl-jp-paramvaluelist
Prints out the elements of a vl-paramvaluelist-p with the enclosing brackets.
Vl-jp-paramdecllist
Prints out the elements of a vl-paramdecllist-p with the enclosing brackets.
Vl-jp-packagelist
Prints out the elements of a vl-packagelist-p with the enclosing brackets.
Vl-jp-namedparamvaluelist
Prints out the elements of a vl-namedparamvaluelist-p with the enclosing brackets.
Vl-jp-namedarglist
Prints out the elements of a vl-namedarglist-p with the enclosing brackets.
Vl-jp-modportlist
Prints out the elements of a vl-modportlist-p with the enclosing brackets.
Vl-jp-modport-portlist
Prints out the elements of a vl-modport-portlist-p with the enclosing brackets.
Vl-jp-modinstlist
Prints out the elements of a vl-modinstlist-p with the enclosing brackets.
Vl-jp-locationlist
Prints out the elements of a vl-locationlist-p with the enclosing brackets.
Vl-jp-interfacelist
Prints out the elements of a vl-interfacelist-p with the enclosing brackets.
Vl-jp-initiallist
Prints out the elements of a vl-initiallist-p with the enclosing brackets.
Vl-jp-gclkdecllist
Prints out the elements of a vl-gclkdecllist-p with the enclosing brackets.
Vl-jp-gateinstlist
Prints out the elements of a vl-gateinstlist-p with the enclosing brackets.
Vl-jp-fwdtypedeflist
Prints out the elements of a vl-fwdtypedeflist-p with the enclosing brackets.
Vl-jp-fwdtypedef
Print the JSON encoding of a vl-fwdtypedef-p to ps.
Vl-jp-fundecllist
Prints out the elements of a vl-fundecllist-p with the enclosing brackets.
Vl-jp-exprdistlist
Prints out the elements of a vl-exprdistlist-p with the enclosing brackets.
Vl-jp-elabtasklist
Prints out the elements of a vl-elabtasklist-p with the enclosing brackets.
Vl-jp-dpiimportlist
Prints out the elements of a vl-dpiimportlist-p with the enclosing brackets.
Vl-jp-dpiexportlist
Prints out the elements of a vl-dpiexportlist-p with the enclosing brackets.
Vl-jp-defaultdisablelist
Prints out the elements of a vl-defaultdisablelist-p with the enclosing brackets.
Vl-jp-covergrouplist
Prints out the elements of a vl-covergrouplist-p with the enclosing brackets.
Vl-jp-clkdecllist
Prints out the elements of a vl-clkdecllist-p with the enclosing brackets.
Vl-jp-clkassignlist
Prints out the elements of a vl-clkassignlist-p with the enclosing brackets.
Vl-jp-clkassign
Print the JSON encoding of a vl-clkassign-p to ps.
Vl-jp-cassertionlist
Prints out the elements of a vl-cassertionlist-p with the enclosing brackets.
Vl-jp-blockitemlist
Prints out the elements of a vl-blockitemlist-p with the enclosing brackets.
Vl-jp-bind
Print the JSON encoding of a vl-bind-p to ps.
Vl-jp-assertionlist
Prints out the elements of a vl-assertionlist-p with the enclosing brackets.
Vl-jp-ansi-portdecllist
Prints out the elements of a vl-ansi-portdecllist-p with the enclosing brackets.
Jp-nat
Encode a probably small natural number as a JSON number.
Vl-jp-udplist
Prints out the elements of a vl-udplist-p with the enclosing brackets.
Vl-jp-udplinelist
Prints out the elements of a vl-udptable-p with the enclosing brackets.
Vl-jp-udpline
Print the JSON encoding of a vl-udpline-p to ps.
Vl-jp-timeunitdecl
Print the JSON encoding of a vl-timeunitdecl-p to ps.
Vl-jp-timeprecisiondecl
Print the JSON encoding of a vl-timeprecisiondecl-p to ps.
Vl-jp-repetition
Print the JSON encoding of a vl-repetition-p to ps.
Vl-jp-repeateventcontrol
Print the JSON encoding of a vl-repeateventcontrol-p to ps.
Vl-jp-regularport
Print the JSON encoding of a vl-regularport-p to ps.
Vl-jp-propspec
Print the JSON encoding of a vl-propspec-p to ps.
Vl-jp-portlist
Prints out the elements of a vl-portlist-p with the enclosing brackets.
Vl-jp-plainarg
Print the JSON encoding of a vl-plainarg-p to ps.
Vl-jp-namedparamvalue
Print the JSON encoding of a vl-namedparamvalue-p to ps.
Vl-jp-namedarg
Print the JSON encoding of a vl-namedarg-p to ps.
Vl-jp-modulelist
Prints out the elements of a vl-modulelist-p with the enclosing brackets.
Vl-jp-modport
Print the JSON encoding of a vl-modport-p to ps.
Vl-jp-initial
Print the JSON encoding of a vl-initial-p to ps.
Vl-jp-importlist
Prints out the elements of a vl-importlist-p with the enclosing brackets.
Vl-jp-import
Print the JSON encoding of a vl-import-p to ps.
Vl-jp-genvarlist
Prints out the elements of a vl-genvarlist-p with the enclosing brackets.
Vl-jp-gclkdecl
Print the JSON encoding of a vl-gclkdecl-p to ps.
Vl-jp-gatestrength
Print the JSON encoding of a vl-gatestrength-p to ps.
Vl-jp-gatedelay
Print the JSON encoding of a vl-gatedelay-p to ps.
Vl-jp-finallist
Prints out the elements of a vl-finallist-p with the enclosing brackets.
Vl-jp-eventcontrol
Print the JSON encoding of a vl-eventcontrol-p to ps.
Vl-jp-distitemlist
Prints out the elements of a vl-distlist-p with the enclosing brackets.
Vl-jp-distitem
Print the JSON encoding of a vl-distitem-p to ps.
Vl-jp-defaultdisable
Print the JSON encoding of a vl-defaultdisable-p to ps.
Vl-jp-covergroup
Print the JSON encoding of a vl-covergroup-p to ps.
Vl-jp-configlist
Prints out the elements of a vl-configlist-p with the enclosing brackets.
Vl-jp-classlist
Prints out the elements of a vl-classlist-p with the enclosing brackets.
Vl-jp-bindlist
Prints out the elements of a vl-bindlist-p with the enclosing brackets.
Vl-jp-assignlist
Prints out the elements of a vl-assignlist-p with the enclosing brackets.
Vl-jp-alwayslist
Prints out the elements of a vl-alwayslist-p with the enclosing brackets.
Vl-jp-always
Print the JSON encoding of a vl-always-p to ps.
Vl-jp-aliaslist
Prints out the elements of a vl-aliaslist-p with the enclosing brackets.
Vl-jp-alias
Print the JSON encoding of a vl-alias-p to ps.
Jp-object
Utility for printing JSON objects, which in some other languages might be called alists, dictionaries, hashes, records, etc.
Vl-jp-udpedge
Print the JSON encoding of a vl-udpedge-p to ps.
Vl-jp-timeliteral
Print the JSON encoding of a vl-timeliteral-p to ps.
Vl-jp-maybe-timeunitdecl
Prints out optional vl-maybe-timeunitdecl-p as either null or type.
Vl-jp-maybe-timeprecisiondecl
Prints out optional vl-maybe-timeprecisiondecl-p as either null or type.
Vl-jp-maybe-gatestrength
Prints out optional vl-maybe-gatestrength-p as either null or type.
Vl-jp-maybe-delayoreventcontrol
Prints out optional vl-maybe-delayoreventcontrol-p as either null or type.
Vl-jp-genvar
Print the JSON encoding of a vl-genvar-p to ps.
Vl-jp-final
Print the JSON encoding of a vl-final-p to ps.
Vl-jp-exprdist
Print the JSON encoding of a vl-exprdist-p to ps.
Vl-jp-delaycontrol
Print the JSON encoding of a vl-delaycontrol-p to ps.
Vl-jp-clkskew
Print the JSON encoding of a vl-clkskew-p to ps.
Vl-jp-maybe-udpsymbol
Prints out optional vl-maybe-udpsymbol-p-p as either null or type.
Vl-jp-maybe-timeliteral
Prints out optional vl-maybe-timeliteral-p as either null or type.
Vl-jp-maybe-scopeid
Prints out optional vl-maybe-scopeid-p as either null or type.
Vl-jp-maybe-rhs
Prints out optional vl-maybe-rhs-p as either null or type.
Vl-jp-maybe-parse-temps
Prints out optional vl-maybe-parse-temps-p as either null or type.
Vl-jp-maybe-paramvalue
Prints out optional vl-maybe-paramvalue-p as either null or type.
Vl-jp-maybe-nettypename
Prints out optional vl-maybe-nettypename-p as either null or type.
Vl-jp-maybe-module
Prints out optional vl-maybe-module-p as either null or type.
Vl-jp-maybe-gatedelay
Prints out optional vl-maybe-gatedelay-p as either null or type.
Vl-jp-maybe-exprdist
Prints out optional vl-maybe-exprdist-p as either null or type.
Vl-jp-maybe-clkskew
Prints out optional vl-maybe-clkskew-p as either null or type.
Vl-jp-elabtask
Print the JSON encoding of a vl-elabtask-p to ps.
Vl-jp-weirdint
Vl-jp-value
Vl-jp-time
Vl-jp-string
Vl-jp-maybe-direction
Vl-jp-maybe-cstrength
Vl-jp-extint
Jp-timeunit
Encode a vl-timeunit-p as a JSON string.
Jp-bool
Encode a booleanp into JSON as true or false.
Jp-bitlist
Encode a vl-bitlist-p as a JSON string.
Jp-bit
Encode a vl-bit-p as a JSON string.
Jp-bignat
Encode a potentially large natural number as a JSON string.
Vl-jp-real
Vl-jp-maybe-exprsign
Vl-jp-gatetype
Vl-jp-exprsign
Vl-jp-evatomtype
Vl-jp-dstrength
Vl-jp-direction
Vl-jp-deassign-type
Vl-jp-cstrength
Vl-jp-casetype
Vl-jp-casekey
Vl-jp-casecheck
Vl-jp-assign-type
Vl-jp-alwaystype
Jp-maybe-string
Jp-maybe-nat
Jp-sym
Optimized version of jp-sym-main.