• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
      • Warnings
      • Primitives
      • Use-set
      • Syntax
      • Getting-started
      • Utilities
      • Loader
      • Transforms
      • Lint
        • Vl-lintconfig-p
        • Lucid
        • Skip-detection
          • Sd-problem-p
          • Sd-keylist-find-skipped
          • Sd-keylist->indicies
          • Sd-key-p
          • Sd-patalist-compare
          • Sd-analyze-ctxexprs
          • Sd-problemlist-p
          • Sd-patalist-p
          • Sd-keygen
          • Sd-patalist
          • Sd-keylist-p
          • Sd-analyze-modulelist
          • Sd-analyze-module-aux
          • Sd-analyze-module
          • Sd-pp-problem-long
          • Sd-analyze-modulelist-aux
          • Sd-problem-score
          • Sd-pp-problem-header
          • Sd-analyze-design
          • Sd-problem->
          • Sd-pp-problem-brief
          • Sd-pp-problemlist-long
          • Sd-pp-problemlist-brief
          • Sd-natlist-linear-increments-p
          • Sd-keylist-linear-increments-p
        • Vl-lintresult-p
        • Lint-warning-suppression
        • Condcheck
        • Selfassigns
        • Leftright-check
        • Dupeinst-check
        • Oddexpr-check
        • Remove-toohard
        • Qmarksize-check
        • Portcheck
        • Duplicate-detect
        • Vl-print-certain-warnings
        • Duperhs-check
        • *vl-lint-help*
        • Lint-stmt-rewrite
        • Drop-missing-submodules
        • Check-case
        • Drop-user-submodules
        • Check-namespace
        • Vl-lint
      • Mlib
      • Server
      • Kit
      • Printer
      • Esim-vl
      • Well-formedness
    • Sv
    • Vwsim
    • Fgl
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Skip-detection

Sd-keygen

(sd-keygen x acc) derives a list of sd-key-ps from x, a wire name, and accumulates them into acc.

Definitions and Theorems

Function: sd-keygen-aux

(defun sd-keygen-aux (n x xl acc)
  (declare (xargs :guard (and (natp n)
                              (natp xl)
                              (stringp x)
                              (= xl (length x))
                              (sd-keylist-p acc))))
  (b* ((n (lnfix n))
       (x (mbe :logic (string-fix x) :exec x))
       (xl (mbe :logic (length x) :exec xl))
       ((when (>= n xl))
        (let* ((x-honsed (hons-copy x))
               (key (make-sd-key :pat x-honsed
                                 :index nil
                                 :orig x-honsed)))
          (cons key acc)))
       (char (char x n))
       ((unless (str::dec-digit-char-p char))
        (sd-keygen-aux (+ 1 n) x xl acc))
       ((mv val len)
        (str::parse-nat-from-string x 0 0 n xl))
       (prefix (subseq x 0 n))
       (suffix (subseq x (min xl (+ n len)) nil))
       (pat (cat prefix "*" suffix))
       (key (make-sd-key :pat (hons-copy pat)
                         :index val
                         :orig x)))
    (sd-keygen-aux (+ len n)
                   x xl (cons key acc))))

Function: sd-keygen

(defun sd-keygen (x acc)
  (declare (xargs :guard (and (stringp x) (sd-keylist-p acc))))
  (sd-keygen-aux 0 x (length x) acc))

Theorem: sd-keylist-p-of-sd-keygen

(defthm sd-keylist-p-of-sd-keygen
  (implies (force (sd-keylist-p acc))
           (sd-keylist-p (sd-keygen x acc))))

Function: sd-keygen-list

(defun sd-keygen-list (x acc)
  (declare (xargs :guard (and (string-listp x)
                              (sd-keylist-p acc))))
  (if (atom x)
      acc
    (let ((acc (sd-keygen (car x) acc)))
      (sd-keygen-list (cdr x) acc))))

Theorem: sd-keylist-p-of-sd-keygen-list

(defthm sd-keylist-p-of-sd-keygen-list
  (implies (force (sd-keylist-p acc))
           (sd-keylist-p (sd-keygen-list x acc))))