• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
    • Vwsim
    • Fgl
    • Vl
    • Svl
      • Svex-simplify
        • Svexlist-simplify
        • Svex-alist-simplify
        • 4vec-to-svex
      • Svl-flatten-design
      • Svl-run
      • Svl-run->svex-alist
      • Svex-to-verilog
    • X86isa
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Svex-simplify

Svexlist-simplify

Try to simplify an sv::svexlist structure with rp::RP-Rewriter using regular rewrite rules about 4vec functions.

Signature

(svexlist-simplify svexlist &key (state 'state) 
                   (rp-state 'rp-state) 
                   (context 'nil) 
                   (runes 'nil) 
                   (reload-rules 't) 
                   (linearize ':auto) 
                   (only-local '4) 
                   (vars-are-integer 't) 
                   (verbose 'nil) 
                   (svex-env-is-var 'nil)) 
 
  → 
(mv res rp::rp-state-res)

Arguments

svexlist — Guard (svexlist-p svexlist).

verbose — Guard (booleanp verbose).

Returns

res — Type (svexlist-p res).

rp::rp-state-res — Type (valid-rp-state-syntaxp rp::rp-state-res), given (if reload-rules (rp::rp-statep rp-state) (valid-rp-state-syntaxp rp-state)) .

Arguments of svexlist-simplify are the same as svex-simplify

Definitions and Theorems

Function: svexlist-simplify-fn

(defun svexlist-simplify-fn
       (svexlist state
                 rp-state context runes reload-rules
                 linearize only-local vars-are-integer
                 verbose svex-env-is-var)
 (declare (xargs :stobjs (state rp-state)))
 (declare (xargs :guard (and (svexlist-p svexlist)
                             (booleanp verbose))))
 (declare
  (xargs
   :guard
   (and
    (or reload-rules
        (valid-rp-state-syntaxp rp-state))
    (or
     (rp::context-syntaxp context)
     (cw
      "ATTENTION!  Given context must satisfy rp::context-syntaxp. Make sure you are giving a translated term ~%")))
   :stobjs (state rp-state)))
 (let ((acl2::__function__ 'svexlist-simplify))
  (declare (ignorable acl2::__function__))
  (b*
   ((linearize (if (eq linearize ':auto)
                   (zp (cons-count-compare svexlist 2048))
                 linearize))
    (rp-state (rp::update-rw-stack nil rp-state))
    ((mv rw rp-state)
     (svexlist-simplify-to-4vec svexlist
                                :state state
                                :context context
                                :runes runes
                                :reload-rules reload-rules
                                :linearize linearize
                                :only-local only-local
                                :vars-are-integer vars-are-integer
                                :verbose verbose
                                :svex-env-is-var svex-env-is-var))
    ((mv err svexlist-res)
     (if only-local (locally-simplified-to-svexlist rw)
       (4vec-to-svex-termlist rw nil linearize)))
    (-
     (and
      err
      (hard-error
       'svexlist-simplify
       "There was a problem while converting the term below to its ~
svex equivalent. Read above for the printed messages. ~p0 ~%"
       (list (cons #\0 rw))))))
   (mv svexlist-res rp-state))))

Theorem: svexlist-p-of-svexlist-simplify.res

(defthm svexlist-p-of-svexlist-simplify.res
  (b* (((mv ?res rp::?rp-state-res)
        (svexlist-simplify-fn svexlist state
                              rp-state context runes reload-rules
                              linearize only-local vars-are-integer
                              verbose svex-env-is-var)))
    (svexlist-p res))
  :rule-classes :rewrite)

Theorem: valid-rp-state-syntaxp-of-svexlist-simplify.rp-state-res

(defthm valid-rp-state-syntaxp-of-svexlist-simplify.rp-state-res
 (implies
   (if reload-rules (rp::rp-statep rp-state)
     (valid-rp-state-syntaxp rp-state))
   (b* (((mv ?res rp::?rp-state-res)
         (svexlist-simplify-fn svexlist state
                               rp-state context runes reload-rules
                               linearize only-local vars-are-integer
                               verbose svex-env-is-var)))
     (valid-rp-state-syntaxp rp::rp-state-res)))
 :rule-classes :rewrite)