Esim
ESIM is a simple, hierarchical, bit-level, cycle-based,
register-transfer level hardware description language. It is based on a clean,
monotonic four-valued logic (see 4v) and features strong support
for symbolic simulation with gl.
Note: ESIM is no longer being actively developed. You
will probably want to instead see its successor, sv.
ESIM is a bit-level ``back-end'' for carrying out hardware verification with
ACL2. It consists of:
- A simplistic, bit-level module representation, ``E modules,'' which are
typically produced from Verilog designs using defmodules.
- A family of functions for ``stepping'' an E module to compute expressions
that capture its next-state and outputs as 4v-sexprs or as faigs;
see esim-steps.
- Mechanisms for describing symbolic runs of a module over multiple clock
phases, such as symbolic-test-vectors.
There is a esim-tutorial that provides a hands-on guide for how to
use vl, esim, and gl together to verify some simple
hardware designs.
Aside from the tutorial, ESIM is not very well documented. An early version
of E is described somewhat in:
Warren A. Hunt, Jr. and Sol Swords. Centaur technology media
unit verification. Case study: Floating point addition. in Computer Aided
Verification (CAV '09), June 2009.
Subtopics
- Symbolic-test-vectors
- A concise way to describe, evaluate, and debug symbolic simulations
of E modules.
- Esim-primitives
- The esim modules that implement vl2014's vl2014::primitives.
- E-conversion
- Translation from simplified Verilog modules into E modules.
- Esim-steps
- Various stepping functions for esim.
- Patterns
- A representation for structured data.
- Mod-internal-paths
- (mod-internal-paths mod) produces a list of paths that describe the
canonical internal wires in a module.
- Defmodules
- High level command to load Verilog files, transform them, and
generate the corresponding E modules.
- Esim-simplify-update-fns
- Pluggable conservative simplifier for ESIM fixpoint extraction
- Esim-tutorial
- The esim hardware verification tutorial.
- Esim-vl
- Functions for working with E modules produced by VL.
