• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • 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
      • Symbolic-test-vector
      • Vl-to-svex
        • Vl-to-sv
        • Vl-design->sv-design
          • Vl-simpconfig
          • Vl-hierarchy-sv-translation
          • Vl-expr-svex-translation
          • Vl-design->svex-modalist
          • Vl-svstmt
            • Vl-svstmt.lisp
              • Vl-casestmt-violation-conds
              • Vl-caselist-none/multiple
              • Vl-elaborated-expr-consteval
              • Vl-always->svex
              • Vl-caseexprs->svex-test
              • Vl-always->svex-checks
              • Vl-implicitvalueparam-final-type
              • Vl-assignstmt->svstmts
              • Vl-fundecl-to-svex
              • Vl-evatomlist-delay-substitution
              • Vl-consteval
              • Vl-alwayslist->svex
              • Vl-index-expr-svex/size/type
              • Vl-vardecllist->svstmts
              • Sv::svex-alist->assigns
              • Vl-case-conservative-test-expr
              • Vl-evatomlist->svex
              • Vl-case-xcond-wrapper
              • Sv::constraintlist-maybe-rewrite-fixpoint
              • Vl-always-apply-trigger-to-updates
              • Vl-initiallist-size-warnings
              • Vl-initial-size-warnings
              • Vl-finallist-size-warnings
              • Vl-always->svex-latch-warnings
              • Vl-final-size-warnings
              • Sv::svarlist-masked-x-subst
              • Sv::svar->lhs-by-mask
              • Svstmt-config
              • Sv::svex-alist-unset-nonblocking
              • Sv::svar->lhs-by-size
              • Combine-mask-alists
              • Sv::svarlist-delay-subst
              • Vttree-constraints-to-svstmts
              • Sv::4vmask-alist-unset-nonblocking
              • Sv::svarlist-remove-delays
              • Vl-caselist->caseexprs
              • Vl-evatomlist-has-edge
        • Vl-to-sv-main
        • Vl-simplify-sv
        • Vl-user-paramsettings->unparam-names
        • Vl-user-paramsettings->modnames
    • Fgl
    • Vwsim
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Vl-svstmt.lisp

Vl-case-conservative-test-expr

Signature

(vl-case-conservative-test-expr test 
                                full-conservative part-conservative) 
 
  → 
full-test

Arguments

test — Guard (sv::svex-p test).

full-conservative — Guard (sv::svex-p full-conservative).

part-conservative — Guard (sv::svex-p part-conservative).

Returns

full-test — Type (sv::svex-p full-test).

Definitions and Theorems

Function: vl-case-conservative-test-expr

(defun vl-case-conservative-test-expr
       (test full-conservative part-conservative)
 (declare (xargs :guard (and (sv::svex-p test)
                             (sv::svex-p full-conservative)
                             (sv::svex-p part-conservative))))
 (let ((__function__ 'vl-case-conservative-test-expr))
  (declare (ignorable __function__))
  (b*
   ((multi-test
      (if (equal (sv::svex-fix part-conservative)
                 0)
          (sv::svex-fix test)
        (sv::svcall sv::bitand test
                    (sv::svcall sv::? part-conservative (sv::svex-x)
                                1))))
    (none-test (if (equal (sv::svex-fix full-conservative)
                          0)
                   multi-test
                 (sv::svcall sv::? full-conservative (sv::svex-x)
                             multi-test))))
   none-test)))

Theorem: svex-p-of-vl-case-conservative-test-expr

(defthm svex-p-of-vl-case-conservative-test-expr
  (b* ((full-test (vl-case-conservative-test-expr
                       test
                       full-conservative part-conservative)))
    (sv::svex-p full-test))
  :rule-classes :rewrite)

Theorem: svex-addr-p-of-vl-case-conservative-test-expr

(defthm svex-addr-p-of-vl-case-conservative-test-expr
 (b* ((?full-test (vl-case-conservative-test-expr
                       test
                       full-conservative part-conservative)))
  (implies
       (and (sv::svarlist-addr-p (sv::svex-vars test))
            (sv::svarlist-addr-p (sv::svex-vars full-conservative))
            (sv::svarlist-addr-p (sv::svex-vars part-conservative)))
       (sv::svarlist-addr-p (sv::svex-vars full-test)))))

Theorem: vl-case-conservative-test-expr-of-svex-fix-test

(defthm vl-case-conservative-test-expr-of-svex-fix-test
  (equal (vl-case-conservative-test-expr
              (sv::svex-fix test)
              full-conservative part-conservative)
         (vl-case-conservative-test-expr
              test
              full-conservative part-conservative)))

Theorem: vl-case-conservative-test-expr-svex-equiv-congruence-on-test

(defthm vl-case-conservative-test-expr-svex-equiv-congruence-on-test
  (implies (sv::svex-equiv test test-equiv)
           (equal (vl-case-conservative-test-expr
                       test
                       full-conservative part-conservative)
                  (vl-case-conservative-test-expr
                       test-equiv
                       full-conservative part-conservative)))
  :rule-classes :congruence)

Theorem: vl-case-conservative-test-expr-of-svex-fix-full-conservative

(defthm vl-case-conservative-test-expr-of-svex-fix-full-conservative
  (equal (vl-case-conservative-test-expr
              test (sv::svex-fix full-conservative)
              part-conservative)
         (vl-case-conservative-test-expr
              test
              full-conservative part-conservative)))

Theorem: vl-case-conservative-test-expr-svex-equiv-congruence-on-full-conservative

(defthm
 vl-case-conservative-test-expr-svex-equiv-congruence-on-full-conservative
 (implies
   (sv::svex-equiv full-conservative
                   full-conservative-equiv)
   (equal
        (vl-case-conservative-test-expr
             test
             full-conservative part-conservative)
        (vl-case-conservative-test-expr test full-conservative-equiv
                                        part-conservative)))
 :rule-classes :congruence)

Theorem: vl-case-conservative-test-expr-of-svex-fix-part-conservative

(defthm vl-case-conservative-test-expr-of-svex-fix-part-conservative
 (equal
   (vl-case-conservative-test-expr test full-conservative
                                   (sv::svex-fix part-conservative))
   (vl-case-conservative-test-expr
        test
        full-conservative part-conservative)))

Theorem: vl-case-conservative-test-expr-svex-equiv-congruence-on-part-conservative

(defthm
 vl-case-conservative-test-expr-svex-equiv-congruence-on-part-conservative
 (implies
   (sv::svex-equiv part-conservative
                   part-conservative-equiv)
   (equal (vl-case-conservative-test-expr
               test
               full-conservative part-conservative)
          (vl-case-conservative-test-expr test full-conservative
                                          part-conservative-equiv)))
 :rule-classes :congruence)