• 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
    • Vwsim
    • Fgl
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Esim-primitives

*esim-notif1*

Primitive E module for a kind of notif1 gate.

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

Definition:

Definition: *esim-notif1*

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