• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Community
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
      • Vl2014
      • Sv
        • Svex-stvs
          • Svtv-data
          • Defsvtv$
          • Svtv-run
          • Defsvtv-phasewise
          • Svtv
          • Svtv-spec
          • Defsvtv
          • Process.lisp
          • Svtv-doc
            • Svtv-to-xml
            • Stv-entry-to-xml
            • Stv-line-to-xml
            • Stv-entries-to-xml
            • Stv-lines-to-xml
            • 4vec-to-bitwise-chars
            • Stv-repeat-last-entry
            • Stv-repeat-last-entries
            • 4vec-to-hex-chars
            • 4vec-to-hex-char
              • Stv-name-to-xml
              • Stv-labels-to-xml
              • 4vec-to-xml-chars
            • Svtv-chase$
            • Svtv-versus-stv
            • Svtv-debug-fsm
            • Structure.lisp
            • Svtv-debug
            • Def-pipeline-thm
            • Expand.lisp
            • Def-cycle-thm
            • Svtv-utilities
            • Svtv-debug$
            • Defsvtv$-phasewise
          • 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
        • Fgl
        • Vwsim
        • Vl
        • X86isa
        • Svl
        • Rtl
      • Software-verification
      • Math
      • Testing-utilities
    • Svtv-doc

    4vec-to-hex-char

    Signature
    (4vec-to-hex-char upper lower) → hex-char
    Arguments
    upper — Guard (natp upper).
    lower — Guard (natp lower).
    Returns
    hex-char — Type (characterp hex-char).

    Definitions and Theorems

    Function: 4vec-to-hex-char

    (defun 4vec-to-hex-char (upper lower)
      (declare (xargs :guard (and (natp upper) (natp lower))))
      (declare (xargs :guard (and (< upper 16) (< lower 16))))
      (let ((__function__ '4vec-to-hex-char))
        (declare (ignorable __function__))
        (b* ((upper (lnfix upper))
             (lower (lnfix lower)))
          (cond ((eql upper lower)
                 (if (< upper 10)
                     (code-char (+ (char-code #\0) upper))
                   (code-char (+ (char-code #\A) (- upper 10)))))
                ((and (eql upper 15) (eql lower 0)) #\X)
                ((and (eql upper 0) (eql lower 15)) #\Z)
                ((eql 0 (logand upper (lognot lower)))
                 #\z)
                (t #\x)))))

    Theorem: characterp-of-4vec-to-hex-char

    (defthm characterp-of-4vec-to-hex-char
      (b* ((hex-char (4vec-to-hex-char upper lower)))
        (characterp hex-char))
      :rule-classes :rewrite)