• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
      • Svex-stvs
      • Svex-fixpoint-decomposition-methodology
      • Sv-versus-esim
      • Svex-decomp
      • Svex-compose-dfs
      • Moddb
      • Svex-compilation
      • Svmods
      • Svstmt
      • Sv-tutorial
        • Stvs-and-testing
        • Decomposition-proofs
        • Proofs-with-stvs
        • Translating-verilog-to-svex
      • Expressions
      • Symbolic-test-vector
      • Vl-to-svex
    • Vwsim
    • Fgl
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Testing-utilities
  • Math

• Sv-tutorial

Translating-verilog-to-svex

How to parse Verilog files and translate them into an svex design

The first step in analyzing a design is to read it in.

The basic function to read and parse a Verilog design is vl::vl-load. The following form shows how to read our ALU design from the file "alu.v".

(defconsts
 (*alu-vl-design* state)
 (b*
    (((mv loadresult state)
      (vl::vl-load (vl::make-vl-loadconfig :start-files '("alu16.v")
                                           :search-path '("lib")))))
    (mv (vl::vl-loadresult->design loadresult)
        state)))

To specify what file(s) to load, we build a vl::vl-loadconfig object. Here we have provided a starting file to read as well as a search path, from which we need to load the flop module. Vl::vl-load produces a vl::vl-loadresult structure, one field of which is the representation of the design, which is the part we're interested in.

Before we go on and translate this into an svex design, we might want to see whether there were any errors in parsing:

(cw-unformatted (vl::vl-reportcard-to-string
                     (vl::vl-design-reportcard *alu-vl-design*)))

This prints the design's "reportcard", the list of warnings about each module. At this point, because our ALU module is well-formed and VL has no trouble parsing it, this doesn't print anything.

The *alu-vl-design* is basically a Verilog parse tree; we want to translate this into an svex module hierarchy. We can do this using vl::vl-design->sv-design:

(defconsts
     (*alu-svex-design* *alu-simplified-good*
                        *alu-simplified-bad*)
     (b* (((mv errmsg svex-design good bad)
           (vl::vl-design->sv-design "alu16" *alu-vl-design*
                                     (vl::make-vl-simpconfig))))
         (and errmsg (raise "~@0~%" errmsg))
         (mv svex-design good bad)))

This runs a series of Verilog to Verilog transforms on the parse tree to simplify it, and finally transforms the simplified hierarchy into an svex design. It returns the resulting svex design, an object of type design, as well as two additional Verilog designs: the portion of the original design that survived the simplification process, and the portion that failed for one reason or another. You can view pretty-printed versions of these:

(cw-unformatted
 (vl::vl-pps-modulelist (vl::vl-design->mods *alu-simplified-bad*)))

doesn't print anything because our module was OK, whereas

(cw-unformatted (vl::vl-pps-modulelist
                     (vl::vl-design->mods *alu-simplified-good*)))

prints out a module similar to the original alu16 module. You can also print its warnings:

(cw-unformatted
     (vl::vl-reportcard-to-string
          (vl::vl-design-reportcard *alu-simplified-good*)))

The svex design *alu-svex-design* is an object of type design, and this is a small enough design that you can print it in full:

(without-evisc *alu-svex-design*)

To continue the ALU example, next see stvs-and-testing.