• 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
        • Rewriting
        • Svex
          • Svar
            • Svar-p
            • Svar-fix
            • Make-svar
            • Svar-equiv
            • Svar->props
            • Svar->delay
            • Svar->bits
            • Change-svar
            • Svarlist
            • Svar->name
            • Svar-map
            • Svar-alist
          • Least-fixpoint
          • Svex-p
          • Svex-select
          • Svex-alist
          • Svex-equiv
          • Svexlist
          • Svex-call
          • Fnsym
          • Svex-quote
          • Svex-var
          • Svcall-rw
          • Svcall
          • Svex-kind
          • Svcall*
          • Svex-fix
          • Svex-count
          • Svex-1z
          • Svex-1x
          • Svex-z
          • Svex-x
        • Bit-blasting
        • Functions
        • 4vmask
        • Why-infinite-width
        • Svex-vars
        • Evaluation
        • Values
      • Symbolic-test-vector
      • Vl-to-svex
    • Vwsim
    • Fgl
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Svar

Svar-p

Recognizer for svar structures.

Signature

(svar-p x) → *

Definitions and Theorems

Function: svar-p

(defun svar-p (x)
 (declare (xargs :guard t))
 (let ((__function__ 'svar-p))
   (declare (ignorable __function__))
   (and (if (atom x)
            (or (stringp x)
                (and (symbolp x) (not (booleanp x))))
          (and (eq (car x) :var)
               (consp (cdr x))
               (let* ((name (cadr x)) (rest (cddr x)))
                 (or (and (integerp rest)
                          (or (not (or (stringp name)
                                       (and (symbolp name)
                                            (not (booleanp name)))))
                              (not (eql 0 rest))))
                     (and (consp rest)
                          (or (and (natp (car rest))
                                   (>= (car rest) 16)
                                   (integerp (cdr rest)))
                              (and (consp (first rest))
                                   (eq (car (first rest)) :delay)
                                   (natp (cdr (first rest)))
                                   (consp (cdr rest))
                                   (consp (second rest))
                                   (eq (car (second rest)) :bits)
                                   (integerp (cdr (second rest)))
                                   (consp (cddr rest)))))))))
        (b* ((?name (if (atom x) x (cadr x)))
             (delay (if (atom x)
                        0
                      (b* ((rest (cddr x))
                           ((when (integerp rest))
                            (loghead 4 rest))
                           ((when (integerp (first rest)))
                            (first rest)))
                        (cdr (first rest)))))
             (bits (if (atom x)
                       0
                     (b* ((rest (cddr x))
                          ((when (integerp rest))
                           (logtail 4 rest))
                          ((when (integerp (first rest)))
                           (cdr rest)))
                       (cdr (second rest)))))
             (props (if (atom x)
                        nil
                      (b* ((rest (cddr x))
                           ((when (integerp rest)) nil)
                           ((when (integerp (first rest))) nil))
                        (cddr rest)))))
          (and (natp delay)
               (integerp bits)
               (svar-proplist-p props))))))