• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
        • Symbolic-test-vectors
          • Defstv
          • Stv-compile
          • Symbolic-test-vector-format
          • Stv-implementation-details
          • Compiled-stv-p
          • Stv-run-for-all-dontcares
          • Stv-run
          • Stv-process
          • Stv-run-check-dontcares
          • Symbolic-test-vector-composition
          • Stv-expand
          • Stv-easy-bindings
          • Stv-debug
          • Stv-run-squash-dontcares
          • Stvdata-p
          • Stv-doc
          • Stv2c
            • Stv2c-opts-p
            • Stv2c-c-symbol-names
            • Stv2c-outs-structdef
            • Stv2c-ins-structdef
            • Stv2c-c-symbol-name
            • Stv2c-header
            • Stv2c-main
          • Stv-widen
          • Stv-out->width
          • Stv-in->width
          • Stv->outs
          • Stv-number-of-phases
          • Stv->ins
          • Stv-suffix-signals
          • Stv->vars
        • 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
    • Testing-utilities
    • Math
  • Symbolic-test-vectors

Stv2c

Naive compiler from symbolic test vectors into C++ code.

Signature
(stv2c argv &key (state 'state)) → state
Arguments
argv — Guard (string-listp argv).

This is a tool for converting symbolic test vectors into C++ programs. Practically speaking, this is just a way to incorporate a Verilog design into some other program.

Our translation is naive in several ways, and we generally don't try to optimize much of anything. In the future, we may work to try to improve performance.

Definitions and Theorems

Function: stv2c-fn

(defun
 stv2c-fn (argv state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (string-listp argv)))
 (let ((__function__ 'stv2c))
      (declare (ignorable __function__))
      (b* (((mv errmsg opts start-files)
            (parse-stv2c-opts argv))
           ((when errmsg)
            (die "~@0~%" errmsg)
            state)
           (opts (change-stv2c-opts opts
                                    :start-files start-files))
           ((stv2c-opts opts) opts)
           ((when opts.help)
            (vl2014::vl-cw-ps-seq (vl2014::vl-print *stv2c-help*))
            (exit-ok)
            state)
           ((when opts.readme)
            (vl2014::vl-cw-ps-seq (vl2014::vl-print *stv2c-readme*))
            (exit-ok)
            state)
           ((when (equal opts.stv ""))
            (die "stv2c: --stv is required.")
            state)
           ((unless (consp opts.start-files))
            (die "stv2c: no Verilog files to process.")
            state)
           (- (cw "stv2c: starting up: ~%"))
           (- (cw " - start files: ~x0~%"
                  opts.start-files))
           (state (vl2014::must-be-regular-files! opts.start-files))
           (- (cw " - stv file: ~x0.~%" opts.stv))
           (state (vl2014::must-be-regular-files! (list opts.stv)))
           (- (cw " - soft heap size ceiling: ~x0 GB~%"
                  opts.mem))
           (- (set-max-mem (* (expt 2 30) opts.mem)))
           (state (stv2c-program opts)))
          (exit-ok)
          state)))

Subtopics

Stv2c-opts-p
Command line options for the stv2c tool.
Stv2c-c-symbol-names
(stv2c-c-symbol-names x) maps stv2c-c-symbol-name across a list.
Stv2c-outs-structdef
Structure definition for the STV outputs.
Stv2c-ins-structdef
Structure definition for the STV inputs.
Stv2c-c-symbol-name
Convert STV input/output names into similar C++ names.
Stv2c-header
Generate the header file for an STV.
Stv2c-main