• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • 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
                • Svstmt-config-fix
                • Svstmt-config-equiv
                • Make-svstmt-config
                • Svstmt-config->uniquecase-constraints
                • Svstmt-config->uniquecase-conservative
                • Svstmt-config->nonblockingp
                • Change-svstmt-config
                • Svstmt-config-p
              • 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

• Svstmt-config

Make-svstmt-config

Basic constructor macro for svstmt-config structures.

Syntax

(make-svstmt-config [:nonblockingp <nonblockingp>] 
                    [:uniquecase-conservative <uniquecase-conservative>] 
                    [:uniquecase-constraints <uniquecase-constraints>]) 

This is the usual way to construct svstmt-config structures. It simply conses together a structure with the specified fields.

This macro generates a new svstmt-config structure from scratch. See also change-svstmt-config, which can "change" an existing structure, instead.

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-svstmt-config

(defmacro make-svstmt-config (&rest args)
  (std::make-aggregate 'svstmt-config
                       args
                       '((:nonblockingp)
                         (:uniquecase-conservative . 0)
                         (:uniquecase-constraints))
                       'make-svstmt-config
                       nil))

Function: svstmt-config

(defun svstmt-config (nonblockingp uniquecase-conservative
                                   uniquecase-constraints)
  (declare (xargs :guard (and (booleanp nonblockingp)
                              (natp uniquecase-conservative)
                              (booleanp uniquecase-constraints))))
  (declare (xargs :guard t))
  (let ((__function__ 'svstmt-config))
    (declare (ignorable __function__))
    (b* ((nonblockingp (mbe :logic (acl2::bool-fix nonblockingp)
                            :exec nonblockingp))
         (uniquecase-conservative
              (mbe :logic (nfix uniquecase-conservative)
                   :exec uniquecase-conservative))
         (uniquecase-constraints
              (mbe :logic (acl2::bool-fix uniquecase-constraints)
                   :exec uniquecase-constraints)))
      (list (cons 'nonblockingp nonblockingp)
            (cons 'uniquecase-conservative
                  uniquecase-conservative)
            (cons 'uniquecase-constraints
                  uniquecase-constraints)))))