• Top
  • Documentation
  • Books
  • 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

Svex-alist-simplify

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

Signature

(svex-alist-simplify x &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

x — Guard (sv::svex-alist-p x).

verbose — Guard (booleanp verbose).

Returns

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: svex-alist-simplify-fn

(defun svex-alist-simplify-fn
       (x 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 (sv::svex-alist-p x)
                             (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__ 'svex-alist-simplify))
   (declare (ignorable acl2::__function__))
   (b* ((svexlist (strip-cdrs x))
        ((mv res rp-state)
         (svexlist-simplify svexlist
                            :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 (pairlis$ (strip-cars x) res)
         rp-state))))

Theorem: valid-rp-state-syntaxp-of-svex-alist-simplify.rp-state-res

(defthm valid-rp-state-syntaxp-of-svex-alist-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)
       (svex-alist-simplify-fn x 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)