• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • 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-z*
          • *esim-del*
          • *esim-cmos*
          • *esim-buf*
          • *esim-zif*
          • *esim-xnor*
          • *esim-t*
          • *esim-safe-mux*
          • *esim-notif0*
          • *esim-nmos*
          • *esim-f*
          • *esim-x*
          • *esim-xor*
          • *esim-unsafe-mux*
          • *esim-tri*
          • *esim-pmos*
          • *esim-or*
          • *esim-not*
            • *esim-notif1*
            • *esim-nor*
            • *esim-nand*
            • *esim-latch*
            • *esim-fsmreg*
            • *esim-bufif1*
            • *esim-bufif0*
            • *esim-and*
            • *esim-primitives*
          • E-conversion
          • Esim-steps
          • Patterns
          • Mod-internal-paths
          • Defmodules
          • Esim-simplify-update-fns
          • Esim-tutorial
          • Esim-vl
        • Vl2014
        • Sv
        • Vwsim
        • Fgl
        • Vl
        • X86isa
        • Svl
        • Rtl
      • Software-verification
      • Testing-utilities
      • Math
    • Esim-primitives

    *esim-not*

    Primitive E module for a NOT gate.

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

    Definition:

    Definition: *esim-not*

    (defconst *esim-not*
              '(:n *esim-not*
                   :x (:out ((|out| not |in|)))
                   :i ((|in|))
                   :o ((|out|))))