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

• Primitives

*vl-1-bit-assign*

Primitive assignment module.

The Verilog definition of this module is:

module VL_1_BIT_ASSIGN (out, in) ;
  output out;
  input in;
  assign out = in;
endmodule

VL takes this as a primitive. This module is also the basis for wider assignment modules; see vl-make-n-bit-assign.

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

Something subtle is that there is probably no way to implement VL_1_BIT_ASSIGN in hardware. One obvious approach would be to use a buffer, but then out would be X when in is Z. Another approach would be to just wire together out and in, but then other assignments to out would also affect in, and in Verilog this isn't the case.

Originally our occform transformation tried to use buffers for assignments since this seemed to be more conservative. But these extra buffers seemed to often be inappropriate, especially when dealing with lower level modules that involve transistors.

Definition: *vl-1-bit-assign*

(defconst *vl-1-bit-assign*
  (b* ((name "VL_1_BIT_ASSIGN")
       (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))
       (assign (make-vl-assign :lvalue out-expr
                               :expr in-expr
                               :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-id*))))