• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
        • Symbolic-test-vectors
        • Esim-primitives
          • *esim-ceq*
          • *esim-id*
          • *esim-del*
          • *esim-buf*
          • *esim-z*
          • *esim-zif*
          • *esim-xnor*
          • *esim-nmos*
          • *esim-cmos*
          • *esim-xor*
          • *esim-unsafe-mux*
          • *esim-t*
          • *esim-tri*
          • *esim-safe-mux*
          • *esim-pmos*
          • *esim-or*
          • *esim-not*
          • *esim-notif1*
          • *esim-notif0*
          • *esim-nor*
          • *esim-nand*
          • *esim-latch*
          • *esim-f*
          • *esim-fsmreg*
          • *esim-bufif1*
            • *esim-bufif0*
            • *esim-and*
            • *esim-x*
            • *esim-primitives*
          • E-conversion
          • Esim-steps
          • Patterns
          • Mod-internal-paths
          • Defmodules
          • Esim-simplify-update-fns
          • Esim-tutorial
          • Esim-vl
        • Vl2014
        • Sv
        • Fgl
        • Vwsim
        • Vl
        • X86isa
        • Svl
        • Rtl
      • Software-verification
      • Math
      • Testing-utilities
    • Esim-primitives

    *esim-bufif1*

    Primitive E module for a kind of bufif1 gate.

    We use this to implement vl2014::*vl-1-bit-bufif1*.

    Definition:

    Definition: *esim-bufif1*

    (defconst *esim-bufif1*
      '(:n *esim-bufif1*
           :x (:out ((|out| tristate |ctrl| |data|)))
           :i ((|data|) (|ctrl|))
           :o ((|out|))))