• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Community
  • 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-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

• Primitives

*vl-1-bit-latch*

Primitive level-sensitive latch.

The Verilog meaning of this module is:

module VL_1_BIT_LATCH (q, clk, d);
   output q;
   input clk;
   input d;
   reg q;

   always @@(d or clk)
     q <= clk ? d : q;

endmodule

VL takes this as a primitive. The always-top transform converts certain always statements into instances of this module.

The corresponding esim primitive is ACL2::*esim-latch*.

Definition: *vl-1-bit-latch*

(defconst *vl-1-bit-latch*
  (b*
    ((name (hons-copy "VL_1_BIT_LATCH"))
     (atts '(("VL_PRIMITIVE") ("VL_HANDS_OFF")))
     ((mv q-expr q-port q-portdecl q-vardecl)
      (vl-primitive-mkport "q" :vl-output))
     ((mv clk-expr
          clk-port clk-portdecl clk-vardecl)
      (vl-primitive-mkport "clk" :vl-input))
     ((mv d-expr d-port d-portdecl d-vardecl)
      (vl-primitive-mkport "d" :vl-input))
     (q-portdecl (change-vl-portdecl q-portdecl
                                     :type *vl-plain-old-reg-type*))
     (q-vardecl (change-vl-vardecl q-vardecl
                                   :type *vl-plain-old-reg-type*))
     (|clk?d:q| (make-vl-nonatom :op :vl-qmark
                                 :args (list clk-expr d-expr q-expr)
                                 :finalwidth 1
                                 :finaltype :vl-unsigned))
     (|q<=clk?d:q| (make-vl-assignstmt :type :vl-nonblocking
                                       :lvalue q-expr
                                       :expr |clk?d:q|
                                       :loc *vl-fakeloc*))
     (d-evatom (make-vl-evatom :type :vl-noedge
                               :expr d-expr))
     (clk-evatom (make-vl-evatom :type :vl-noedge
                                 :expr clk-expr))
     (@d-or-clk
          (make-vl-eventcontrol :starp nil
                                :atoms (list d-evatom clk-evatom)))
     (stmt (make-vl-timingstmt :ctrl @d-or-clk
                               :body |q<=clk?d:q|))
     (always (make-vl-always :type :vl-always
                             :stmt stmt
                             :loc *vl-fakeloc*)))
    (hons-copy
         (make-vl-module
              :name name
              :origname name
              :ports (list q-port clk-port d-port)
              :portdecls (list q-portdecl clk-portdecl d-portdecl)
              :vardecls (list q-vardecl clk-vardecl d-vardecl)
              :alwayses (list always)
              :minloc *vl-fakeloc*
              :maxloc *vl-fakeloc*
              :atts atts
              :esim acl2::*esim-latch*))))