• 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-chase$
        • Svtv-versus-stv
        • Svtv-debug-fsm
        • Structure.lisp
        • Svtv-debug
        • Def-pipeline-thm
        • Expand.lisp
          • Svtv-parse-path-indices
          • Svtv-extend-entrylist
          • Svtv-parse-path/select-aux
          • Svtv-fsm-add-names
          • Svtv-1wire->lhs
          • Svtv-wires->lhses
          • Svtv-concat->lhs
          • Svtv-wire->lhs!
          • Svtv-lines->overrides
          • Svtv-wire->lhs
          • Svtv-mod-alias-guard
          • Svtv-fsm-mod-alias-guard
          • Svtv-parse-path/select
          • Svtv-expand-lines
          • Svtv-max-length
          • Msg-list
        • 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

• Expand.lisp

Svtv-parse-path/select-aux

Signature

(svtv-parse-path/select-aux dotted-parts orig-x) 
  → 
(mv errmsg path range-msb range-lsb)

Arguments

dotted-parts — Guard (string-listp dotted-parts).

orig-x — Guard (stringp orig-x).

Returns

path — Type (implies (not errmsg) (path-p path)).

range-msb — Type (or (not range-msb) (natp range-msb)).

range-lsb — Type (implies range-msb (natp range-lsb)).

Definitions and Theorems

Function: svtv-parse-path/select-aux

(defun svtv-parse-path/select-aux (dotted-parts orig-x)
  (declare (xargs :guard (and (string-listp dotted-parts)
                              (stringp orig-x))))
  (let ((__function__ 'svtv-parse-path/select-aux))
    (declare (ignorable __function__))
    (b* ((orig-x (mbe :logic (str-fix orig-x)
                      :exec orig-x))
         ((when (atom dotted-parts))
          (mv (msg "Error -- empty wire path? \"~s0\""
                   orig-x)
              nil nil nil))
         (lastp (atom (cdr dotted-parts)))
         (part1 (mbe :logic (str-fix (car dotted-parts))
                     :exec (car dotted-parts)))
         ((unless (and (not (equal part1 ""))
                       (eql (char part1 (1- (length part1)))
                            #\])))
          (b* (((when lastp)
                (mv nil (make-path-wire :name part1)
                    nil nil))
               ((mv errmsg rest range-msb range-lsb)
                (svtv-parse-path/select-aux (cdr dotted-parts)
                                            orig-x))
               ((when errmsg) (mv errmsg nil nil nil)))
            (mv nil
                (make-path-scope :subpath rest
                                 :namespace part1)
                range-msb range-lsb)))
         (lbrack-pos (strpos "[" part1))
         ((unless lbrack-pos)
          (mv (msg "Found ] without previous [: \"~s0\" inside \"~s1\""
                   part1 orig-x)
              nil nil nil))
         (name-part (subseq part1 0 lbrack-pos))
         (bracketed-part (subseq part1 lbrack-pos nil))
         (bracketed-parts (strtok bracketed-part '(#\])))
         ((unless bracketed-parts)
          (mv "This shouldn't happen." nil nil nil))
         ((mv err index-path range-msb range-lsb)
          (svtv-parse-path-indices bracketed-parts lastp orig-x))
         ((when err) (mv err nil nil nil))
         ((when lastp)
          (mv nil
              (if index-path (make-path-scope :namespace name-part
                                              :subpath index-path)
                (make-path-wire :name name-part))
              range-msb range-lsb))
         ((mv err rest-path range-msb range-lsb)
          (svtv-parse-path/select-aux (cdr dotted-parts)
                                      orig-x))
         ((when err) (mv err nil nil nil)))
      (mv nil
          (make-path-scope
               :namespace name-part :subpath
               (if index-path (path-append index-path rest-path)
                 rest-path))
          range-msb range-lsb))))

Theorem: return-type-of-svtv-parse-path/select-aux.path

(defthm return-type-of-svtv-parse-path/select-aux.path
  (b* (((mv ?errmsg ?path ?range-msb ?range-lsb)
        (svtv-parse-path/select-aux dotted-parts orig-x)))
    (implies (not errmsg) (path-p path)))
  :rule-classes :rewrite)

Theorem: return-type-of-svtv-parse-path/select-aux.range-msb

(defthm return-type-of-svtv-parse-path/select-aux.range-msb
  (b* (((mv ?errmsg ?path ?range-msb ?range-lsb)
        (svtv-parse-path/select-aux dotted-parts orig-x)))
    (or (not range-msb) (natp range-msb)))
  :rule-classes :type-prescription)

Theorem: return-type-of-svtv-parse-path/select-aux.range-lsb

(defthm return-type-of-svtv-parse-path/select-aux.range-lsb
  (b* (((mv ?errmsg ?path ?range-msb ?range-lsb)
        (svtv-parse-path/select-aux dotted-parts orig-x)))
    (implies range-msb (natp range-lsb)))
  :rule-classes :type-prescription)

Theorem: svtv-parse-path/select-aux-of-string-list-fix-dotted-parts

(defthm svtv-parse-path/select-aux-of-string-list-fix-dotted-parts
 (equal
     (svtv-parse-path/select-aux (str::string-list-fix dotted-parts)
                                 orig-x)
     (svtv-parse-path/select-aux dotted-parts orig-x)))

Theorem: svtv-parse-path/select-aux-string-list-equiv-congruence-on-dotted-parts

(defthm
 svtv-parse-path/select-aux-string-list-equiv-congruence-on-dotted-parts
 (implies
     (str::string-list-equiv dotted-parts dotted-parts-equiv)
     (equal (svtv-parse-path/select-aux dotted-parts orig-x)
            (svtv-parse-path/select-aux dotted-parts-equiv orig-x)))
 :rule-classes :congruence)

Theorem: svtv-parse-path/select-aux-of-str-fix-orig-x

(defthm svtv-parse-path/select-aux-of-str-fix-orig-x
  (equal (svtv-parse-path/select-aux dotted-parts (str-fix orig-x))
         (svtv-parse-path/select-aux dotted-parts orig-x)))

Theorem: svtv-parse-path/select-aux-streqv-congruence-on-orig-x

(defthm svtv-parse-path/select-aux-streqv-congruence-on-orig-x
 (implies
     (acl2::streqv orig-x orig-x-equiv)
     (equal (svtv-parse-path/select-aux dotted-parts orig-x)
            (svtv-parse-path/select-aux dotted-parts orig-x-equiv)))
 :rule-classes :congruence)