• 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

• Svl

Svex-to-verilog

Export an SVEX to a Verilog file

Dumps a Verilog file based on a given sv::svex

Use: (svex-to-verilog svex &key (output-file-name '"test") (out-wrapper 'nil) (input-vars 'nil) (env 'nil) (assume ''t) (export-to-svexl 'nil) (sanity-check 't) (skip-svex-simplify 'nil) (skip-dumping-to-verilog 'nil))

This calls svex-alist-to-verilog by creating a faux output variable svl::_out.

Example call:

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

See svex-alist-to-verilog for more details.

Subtopics

Svex-alist-to-verilog

Export an SVEX-ALIST to a Verilog file

Svtv-to-verilog

Export an SVTV instance to a Verilog file