Naive compiler from symbolic test vectors into C++ code.
(stv2c argv &key (state 'state)) → state
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.
Function:
(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)))