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.
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.