• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Debugging
  • Projects
  • 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-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
    • Vwsim
    • Fgl
    • Vl
    • Svl
    • X86isa
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Primitives

*vl-1-bit-delay-1*

Primitive assignment with delay.

The Verilog definition of this module is:

module VL_1_BIT_DELAY_1 (out, in) ;
  output out;
  input in;
  assign #1 out = in;
endmodule

VL takes this as a primitive. It is used by our delayredux transform to separate delays from assignment statements.

The corresponding esim primitive is ACL2::*esim-del*, but note that esim really has no notion of delays and this ends up being equivalent to an ordinary *vl-1-bit-assign*.

Definition: *vl-1-bit-delay-1*

(defconst *vl-1-bit-delay-1*
  (b* ((name "VL_1_BIT_DELAY_1")
       (atts '(("VL_PRIMITIVE") ("VL_HANDS_OFF")))
       ((mv out-expr
            out-port out-portdecl out-vardecl)
        (vl-primitive-mkport "out" :vl-output))
       ((mv in-expr in-port in-portdecl in-vardecl)
        (vl-primitive-mkport "in" :vl-input))
       (one (vl-make-index 1))
       (delay (make-vl-gatedelay :rise one
                                 :fall one
                                 :high one))
       (assign (make-vl-assign :lvalue out-expr
                               :expr in-expr
                               :delay delay
                               :loc *vl-fakeloc*)))
    (hons-copy
         (make-vl-module :name name
                         :origname name
                         :ports (list out-port in-port)
                         :portdecls (list out-portdecl in-portdecl)
                         :vardecls (list out-vardecl in-vardecl)
                         :assigns (list assign)
                         :minloc *vl-fakeloc*
                         :maxloc *vl-fakeloc*
                         :atts atts
                         :esim acl2::*esim-del*))))