• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
      • Warnings
      • Primitives
        • *vl-1-bit-approx-mux*
        • *vl-1-bit-mux*
        • Nedgeflop
          • Vl-make-same-bitselect-from-each
          • Vl-primitive-mkports
          • Vl-nedgeflop-ifstmt
          • Vl-make-1-bit-n-edge-flop
          • Vl-make-nedgeflop-insts
          • Vl-nedgeflop-always
          • Vl-nedgeflop-clkedge-assigns
          • Vl-nedgeflop-update-sexpr
          • Vl-nedgeflop-e-wires
          • Vl-make-delay-assigns
          • Vl-nedgeflop-posedge-clks
          • Vl-nedgeflop-data-mux
          • Vl-nedgeflop-some-edge-sexpr
          • Vl-modinsts-add-atts
          • Vl-nedgeflop-or-edges
        • Vl-primitive-mkport
        • *vl-1-bit-assign*
        • *vl-1-bit-zmux*
        • Vl-primitive-mkwire
        • *vl-1-bit-bufif1*
        • *vl-1-bit-bufif0*
        • *vl-1-bit-delay-1*
        • *vl-1-bit-ceq*
        • *vl-1-bit-buf*
        • *vl-1-bit-rcmos*
        • *vl-1-bit-latch*
        • *vl-1-bit-cmos*
        • *vl-1-bit-power*
        • *vl-1-bit-rpmos*
        • *vl-1-bit-rnmos*
        • *vl-1-bit-pmos*
        • *vl-1-bit-nmos*
        • *vl-1-bit-ground*
        • *vl-1-bit-tranif1*
        • *vl-1-bit-tranif0*
        • *vl-1-bit-rtranif1*
        • *vl-1-bit-rtranif0*
        • *vl-1-bit-rtran*
        • *vl-1-bit-tran*
        • *vl-1-bit-notif1*
        • *vl-1-bit-notif0*
        • *vl-1-bit-and*
        • *vl-1-bit-xor*
        • *vl-1-bit-xnor*
        • *vl-1-bit-pullup*
        • *vl-1-bit-pulldown*
        • *vl-1-bit-or*
        • *vl-1-bit-not*
        • *vl-1-bit-nor*
        • *vl-1-bit-nand*
        • *vl-1-bit-z*
        • *vl-1-bit-x*
        • *vl-1-bit-t*
        • *vl-1-bit-f*
      • Use-set
      • Syntax
      • Getting-started
      • Utilities
      • Loader
      • Transforms
      • Lint
      • Mlib
      • Server
      • Kit
      • Printer
      • Esim-vl
      • Well-formedness
    • Sv
    • Fgl
    • Vwsim
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Nedgeflop

Vl-nedgeflop-always

Build the Verilog always statement for a primitive n-edge flop.

Signature

(vl-nedgeflop-always q-expr clk-exprs data-exprs) → always

Arguments

q-expr — e.g., q.
    Guard (vl-expr-p q-expr).

clk-exprs — e.g., (clk0 clk1 clk2).
    Guard (vl-exprlist-p clk-exprs).

data-exprs — e.g., (d0 d1 d2).
    Guard (vl-exprlist-p data-exprs).

Returns

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

Definitions and Theorems

Function: vl-nedgeflop-always

(defun vl-nedgeflop-always (q-expr clk-exprs data-exprs)
  (declare (xargs :guard (and (vl-expr-p q-expr)
                              (vl-exprlist-p clk-exprs)
                              (vl-exprlist-p data-exprs))))
  (declare (xargs :guard (and (consp clk-exprs)
                              (same-lengthp clk-exprs data-exprs))))
  (let ((__function__ 'vl-nedgeflop-always))
    (declare (ignorable __function__))
    (b* ((evatoms (vl-nedgeflop-posedge-clks clk-exprs))
         (evctrl (make-vl-eventcontrol :starp nil
                                       :atoms evatoms))
         (body (vl-nedgeflop-ifstmt q-expr clk-exprs data-exprs))
         (stmt (make-vl-timingstmt :ctrl evctrl
                                   :body body)))
      (make-vl-always :type :vl-always
                      :stmt stmt
                      :loc *vl-fakeloc*))))

Theorem: vl-always-p-of-vl-nedgeflop-always

(defthm vl-always-p-of-vl-nedgeflop-always
 (implies
    (and (force (vl-expr-p q-expr))
         (force (vl-exprlist-p clk-exprs))
         (force (vl-exprlist-p data-exprs))
         (force (consp clk-exprs))
         (force (same-lengthp clk-exprs data-exprs)))
    (b* ((always (vl-nedgeflop-always q-expr clk-exprs data-exprs)))
      (vl-always-p always)))
 :rule-classes :rewrite)