• 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
      • Rtl
    • Software-verification
    • Math
    • Testing-utilities
  • Hardware-verification

Svl

A framework to simulate Verilog designs with retained design hiearchy

Similar to sv::svtv, SVL semantics is converted from sv to simulate Verilog designs but it can retain design hierarchy by not flattening and composing selected modules. It supports combinational and sequential circuits but it fails in case of combinational loops.

You need vl and sv designs to create SVL designs. You can use functions svl-flatten-design to create SVL design, and svl-run to run the generated design.

Using the SVL system, you can perform hierarchical reasoning on Verilog designs. For combinational submodules, you can have a rewrite rule replacing svl-run-phase-wog instance of that submodule with its specification, and that rule can be applied when rewriting the main module. See rp::multiplier-verification for a use case.

DISCLAIMER: SVL IS NOT MAINTAINED ANYMORE AND WAS ONLY AN EXPERIMENTAL LIBRARY.

Subtopics

Svex-simplify
Try to simplify an sv::svex structure with ACL2::rp-rewriter using regular rewrite rules about 4vec functions.
Svl-flatten-design
Generate SVL designs from SV and VL Designs
Svl-run
Evaluate SVL designs
Svl-run->svex-alist
Convert an SVL design to an sv::svex-alist.
Svex-to-verilog
Export an SVEX to a Verilog file