• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
      • Warnings
      • Primitives
      • Use-set
      • Syntax
      • Getting-started
      • Utilities
      • Loader
      • Transforms
        • Expression-sizing
        • Occform
        • Oprewrite
        • Expand-functions
        • Delayredux
        • Unparameterization
        • Caseelim
        • Split
        • Selresolve
        • Weirdint-elim
        • Vl-delta
        • Replicate-insts
        • Rangeresolve
        • Propagate
        • Clean-selects
        • Clean-params
        • Blankargs
        • Inline-mods
        • Expr-simp
        • Trunc
        • Always-top
        • Gatesplit
        • Gate-elim
        • Expression-optimization
        • Elim-supplies
        • Wildelim
        • Drop-blankports
        • Clean-warnings
        • Addinstnames
        • Custom-transform-hooks
        • Annotate
        • Latchcode
          • Vl-latchcode-synth-always
          • Vl-match-latch-main
          • Vl-careful-match-latch
          • Vl-careless-match-latch
          • Vl-latchcode-synth-alwayses
          • Vl-make-n-bit-latch-vec
          • Vl-make-n-bit-latch
        • Elim-unused-vars
        • Problem-modules
      • Lint
      • Mlib
      • Server
      • Kit
      • Printer
      • Esim-vl
      • Well-formedness
    • Sv
    • Vwsim
    • Fgl
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Latchcode

Vl-latchcode-synth-alwayses

Signature

(vl-latchcode-synth-alwayses x scary-regs 
                             vars cvtregs delta careful-p vecp) 
 
  → 
(mv new-x cvtregs delta)

Arguments

x — Guard (vl-alwayslist-p x).

scary-regs — Guard (and (string-listp scary-regs) (setp scary-regs)).

vars — Guard (vl-vardecllist-p vars).

cvtregs — Guard (string-listp cvtregs).

delta — Guard (vl-delta-p delta).

careful-p — Guard (booleanp careful-p).

Returns

new-x — Type (vl-alwayslist-p new-x), given the guard.

cvtregs — Type (string-listp cvtregs), given the guard.

delta — Type (vl-delta-p delta), given the guard.

Definitions and Theorems

Function: vl-latchcode-synth-alwayses

(defun vl-latchcode-synth-alwayses
       (x scary-regs
          vars cvtregs delta careful-p vecp)
 (declare (xargs :guard (and (vl-alwayslist-p x)
                             (and (string-listp scary-regs)
                                  (setp scary-regs))
                             (vl-vardecllist-p vars)
                             (string-listp cvtregs)
                             (vl-delta-p delta)
                             (booleanp careful-p))))
 (let ((__function__ 'vl-latchcode-synth-alwayses))
   (declare (ignorable __function__))
   (b*
    (((when (atom x)) (mv nil cvtregs delta))
     ((mv new-car? cvtregs delta)
      (vl-latchcode-synth-always (car x)
                                 scary-regs
                                 vars cvtregs delta careful-p vecp))
     ((mv new-cdr cvtregs delta)
      (vl-latchcode-synth-alwayses
           (cdr x)
           scary-regs
           vars cvtregs delta careful-p vecp))
     (new-x (if new-car? (cons new-car? new-cdr)
              new-cdr)))
    (mv new-x cvtregs delta))))

Theorem: vl-alwayslist-p-of-vl-latchcode-synth-alwayses.new-x

(defthm vl-alwayslist-p-of-vl-latchcode-synth-alwayses.new-x
  (implies (and (force (vl-alwayslist-p x))
                (force (if (string-listp scary-regs)
                           (setp scary-regs)
                         'nil))
                (force (vl-vardecllist-p vars))
                (force (string-listp cvtregs))
                (force (vl-delta-p delta))
                (force (booleanp careful-p)))
           (b* (((mv ?new-x ?cvtregs ?delta)
                 (vl-latchcode-synth-alwayses
                      x scary-regs
                      vars cvtregs delta careful-p vecp)))
             (vl-alwayslist-p new-x)))
  :rule-classes :rewrite)

Theorem: string-listp-of-vl-latchcode-synth-alwayses.cvtregs

(defthm string-listp-of-vl-latchcode-synth-alwayses.cvtregs
  (implies (and (force (vl-alwayslist-p x))
                (force (if (string-listp scary-regs)
                           (setp scary-regs)
                         'nil))
                (force (vl-vardecllist-p vars))
                (force (string-listp cvtregs))
                (force (vl-delta-p delta))
                (force (booleanp careful-p)))
           (b* (((mv ?new-x ?cvtregs ?delta)
                 (vl-latchcode-synth-alwayses
                      x scary-regs
                      vars cvtregs delta careful-p vecp)))
             (string-listp cvtregs)))
  :rule-classes :rewrite)

Theorem: vl-delta-p-of-vl-latchcode-synth-alwayses.delta

(defthm vl-delta-p-of-vl-latchcode-synth-alwayses.delta
  (implies (and (force (vl-alwayslist-p x))
                (force (if (string-listp scary-regs)
                           (setp scary-regs)
                         'nil))
                (force (vl-vardecllist-p vars))
                (force (string-listp cvtregs))
                (force (vl-delta-p delta))
                (force (booleanp careful-p)))
           (b* (((mv ?new-x ?cvtregs ?delta)
                 (vl-latchcode-synth-alwayses
                      x scary-regs
                      vars cvtregs delta careful-p vecp)))
             (vl-delta-p delta)))
  :rule-classes :rewrite)