• 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

Esim-primitives

The esim modules that implement vl2014's vl2014::primitives.

The patterns used for the :i and :o ports here might look strange. For instance, why do we use ((|a|) (|b|)) as the input pattern for an AND gate instead of (|a| |b|)? This allows our primitives to be directly compatible with VL's primitives, as far as vl2014::vl-portdecls-to-i/o is concerned.

BOZO Things to consider:

  • Do we want to add NAND and NOR primitives to 4v-sexprs? We currently implement them as (not (and a b)) and (not (or a b)).
  • Do we want to change LATCH and FLOP to use 4v-ite* instead of 4v-ite? It probably won't help with combinational loops at all, but it may make our modeling more conservative. If it doesn't cause problems, it might be worth doing.
  • Is there any good reason to keep PULLUP and ID in 4v-sexprs? We aren't using them for anything.
  • Eventaully implement WOR and WAND resolution

Subtopics

*esim-ceq*
Primitive E module for a Verilog === operator.
*esim-id*
Primitive E module for identity assignment.
*esim-del*
Primitive E module for a delayed assignment.
*esim-buf*
Primitive E module for a BUF gate.
*esim-z*
Primitive E module for producing Z.
*esim-zif*
Primitive E module for a kind of pass-gate style mux.
*esim-xnor*
Primitive E module for an XNOR gate.
*esim-nmos*
Primitive E module for a kind of nmos gate.
*esim-cmos*
Primitive E module for a kind of cmos gate.
*esim-xor*
Primitive E module for an XOR gate.
*esim-unsafe-mux*
Primitive E module for a (less conservative) mux.
*esim-t*
Primitive E module for producing T.
*esim-tri*
Primitive E module for a tri-state buffer.
*esim-safe-mux*
Primitive E module for a (more conservative) mux.
*esim-pmos*
Primitive E module for a kind of pmos gate.
*esim-or*
Primitive E module for an OR gate.
*esim-not*
Primitive E module for a NOT gate.
*esim-notif1*
Primitive E module for a kind of notif1 gate.
*esim-notif0*
Primitive E module for a kind of notif0 gate.
*esim-nor*
Primitive E module for a NOR gate.
*esim-nand*
Primitive E module for a NAND gate.
*esim-latch*
Primitive E module for a latch.
*esim-f*
Primitive E module for producing F.
*esim-fsmreg*
Primitive E module for an unclocked register.
*esim-bufif1*
Primitive E module for a kind of bufif1 gate.
*esim-bufif0*
Primitive E module for a kind of bufif0 gate.
*esim-and*
Primitive E module for an AND gate.
*esim-x*
Primitive E module for producing X.
*esim-primitives*
A list of all esim primitives.