		Search-engine friendly clone of the ACL2 documentation.

Vl-zip

Vl-zipfile

Representation of a .vlzip file's contents. These files can be used to store pre-parsed Verilog designs.

This is a product type introduced by defprod.

Fields

name — stringp: A name for this project.
syntax — stringp: Syntax version for the VL that created this file.
date — stringp: Date stamp for when the file was created.
ltime — natp: Lisp timestamp for when this file was created.
design — vl-design: The SystemVerilog design we have captured.
filemap — vl-filemap: Raw contents of the actual files that were loaded.
defines — vl-defines: Ending `defines after preprocessing.

This is the file format used by the vl-server. It contains a pre-parsed Verilog design, all the source code used to create it, and other information.

We write out vl-zipfile structures in a special format so that we can read the VL syntax version, creation date, and design name without having to read the contents of the design. This allows us to (in the VL server) quickly recognize which .vlzip files are compatible with our current syntax version.

Subtopics

Vl-zipfile-fix: Fixing function for vl-zipfile structures.
Vl-read-zip-header: Read only the header information out of a vlzip file.
Vl-maybe-zipfile: Option type; vl-zipfile or nil.
Vl-read-zip: Read a whole vlzip file.
Make-vl-zipfile: Basic constructor macro for vl-zipfile structures.
Vl-zipfile-equiv: Basic equivalence relation for vl-zipfile structures.
Vl-zipfile-p: Recognizer for vl-zipfile structures.
Change-vl-zipfile: Modifying constructor for vl-zipfile structures.
Vl-zipfile->syntax: Get the syntax field from a vl-zipfile.
Vl-zipfile->filemap: Get the filemap field from a vl-zipfile.
Vl-zipfile->design: Get the design field from a vl-zipfile.
Vl-zipfile->defines: Get the defines field from a vl-zipfile.
Vl-zipfile->name: Get the name field from a vl-zipfile.
Vl-zipfile->ltime: Get the ltime field from a vl-zipfile.
Vl-zipfile->date: Get the date field from a vl-zipfile.
Vl-write-zip