• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
    • Fgl
    • Vwsim
    • Vl
    • X86isa
    • Svl
      • Svex-simplify
      • Svl-flatten-design
      • Svl-run
      • Svl-run->svex-alist
      • Svex-to-verilog
        • Svex-alist-to-verilog
        • Svtv-to-verilog
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Svex-to-verilog

Svtv-to-verilog

Export an SVTV instance to a Verilog file

Dumps a Verilog file based on a given sv::defsvtv$

This calls svex-alist-to-verilog by extracting svex-alist from SVTV. Please see svex-alist-to-verilog for more details. Example use:

(svl::svtv-to-verilog (my-svtv)
                      :output-file-name "test"
                      :output-vars (my-out)
                      :out-wrappers '((my-out . (sv::partsel 4 4 my-out)))
                      :input-vars (srca)
                      :env `((srcb . 0) (srcc . 0) (srcd . 0))
                      :assume (and (equal (svl::bits srca 24 1) 0))
                      :skip-svex-simplify nil)