Sv
SV is a hardware verification library that features a vector-based
expression representation (svex), efficient symbolic simulation that is
integrated with gl, and support for many SystemVerilog features. It
generally replaces esim as a backend for vl.
SV is an ACL2 library for hardware verification, developed at Centaur
Technology, primarily by Sol Swords. It is the latest in a long line of
hardware description languages that are deeply embedded within ACL2: it
replaces Centaur's esim, which itself succeeded the E language of Hunt
& Boyer, which was a descendant of DE2 (Hunt & Reeber), which followed
from DUAL-EVAL (Hunt & Brock). For a brief comparison, see sv-versus-esim.
SV combines and integrates several major components:
- Expression language. At its core, SV is based on a language of
symbolic expressions that represent functions over infinite-width
vectors of four-valued ``bits.'' We define a sensible semantics for these
expressions (svex-eval) and implement tools like rewriting for
simplifying these expressions in provably sound ways. We also provide special
support for bit-blasting SV expressions with gl and fgl::fgl,
which allows you to
process them with efficient ACL2::boolean-reasoning tools like ACL2::aignet, ACL2::satlink, ACL2::ubdds, etc.
- Modules and compilation. SV has a simple, svex-based
representation for hardware modules. It also has a compiler that can assemble
these modules into a convenient finite state machine (FSM) representation, with
well-defined semantics, and with full observability of all parts of the
original design. This compilation process involves, e.g., flattening the
module hierarchy, resolving multiply driven wires, etc.; see svex-compilation.
- SystemVerilog/Verilog loading. SV is integrated with vl so
that you can translate SystemVerilog and Verilog designs into its internal SV
representation. In practice, this is the main way to get the SV modules to
analyze.
- Proof development and debugging. SV provides tools like svex-stvss for running modules, which allow you to supply inputs and extract
outputs at particular times. These user-interfacing tools can be used in ACL2
theorems and provide debugging conveniences such as generating VCD files for
use with waveform viewers.
This documentation is mainly a reference. New users should probably start
with the sv-tutorial, which gives a tour of using SV to verify some
simple Verilog designs. (This tutorial will be quite familiar if you have used
esim in the past.)
Subtopics
- Svex-stvs
- SVEX Symbolic Test Vectors
- Svex-decomposition-methodology
- High-level description of decomposition methodology for svtvs.
- Sv-versus-esim
- A quick comparison of sv and its predecessor, esim.
- Svex-decomp
- (Deprecated) Proving that a decomposition is equivalent to some whole.
- Svex-compose-dfs
- Compose together a network of svex assignments, stopping when a
variable depends on itself.
- Svex-compilation
- Turning a hierarchical SVEX design into a finite state machine.
- Moddb
- A database object that provides a unique numbering of all the wires in
a module hierarchy.
- Svmods
- An svex-based format for expressing a module hierarchy.
- Svstmt
- An svex-based representation for procedural statement blocks
- Sv-tutorial
- Basic tutorial: how to use the svex package to do datapath verification.
- Expressions
- The Symbolic Vector Expression language (SVEX)
forms the core of SV. It includes an S-expression language for certain
pre-defined hardware functions, an interpreter for evaluating these expressions
on four-valued integers, and related tools.
- Symbolic-test-vector
- An object describing a finite run of a hardware model.
- Vl-to-svex
- Translation of vl designs into an SVEX design.
