• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Community
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
      • Vl2014
      • Sv
        • Svex-stvs
        • Svex-decomposition-methodology
        • Sv-versus-esim
        • Svex-decomp
        • Svex-compose-dfs
        • Svex-compilation
        • Moddb
        • Svmods
        • Svstmt
        • Sv-tutorial
        • Expressions
        • Symbolic-test-vector
        • Vl-to-svex
          • Vl-to-sv
          • Vl-design->sv-design
            • Vl-simpconfig
            • Vl-hierarchy-sv-translation
            • Vl-expr-svex-translation
              • Sv::vl-expr.lisp
              • Vttree
            • Vl-design->svex-modalist
            • Vl-svstmt
          • Vl-to-sv-main
          • Vl-simplify-sv
          • Vl-user-paramsettings->unparam-names
          • Vl-user-paramsettings->modnames
      • Fgl
      • Vwsim
      • Vl
      • X86isa
      • Svl
      • Rtl
    • Software-verification
    • Math
    • Testing-utilities
  • Vl-design->sv-design

Vl-expr-svex-translation

Compilation from (sized) vl expressions into sv::svex expressions.

There are several top-level functions for converting a VL expression into a sv::svex expression, including vl-expr-to-svex-untyped, vl-expr-to-svex-selfdet, and vl-expr-to-svex-maybe-typed.

We assume that the expressions we are dealing with are sized.

The Garbage Convention. Our goal is to produce svex expressions that are "correct" at least for this size. We don't care about the bits that are "past" the expression's final width.

For example, if we are converting 3'b100 into an svex expression, it would be valid to just use (concat 3 #b100 anything).

This has widespread consequences.

In many cases, we don't have to worry about the upper bits, because we know, for instance, that after sizing, in a VL expression like a & b, that the widths of a and b agree with the final width of the whole a & b expression. So any "garbage" in the upper bits can only affect the upper bits of the result.

However, in certain cases we have to be more careful. For instance, if we are translating a < b, then the svex semantics are that we do an infinite width comparison, so we need to be careful to properly sign/zero extend the two arguments to their appropriate, final value.

Why do it this way? Some possible alternatives:

  • Force everything past the final width to X.
  • Sign/zero extend everything so that every expression is correct out to infinite width.

Forcing the high bits to X has some appeal: it would be nice to know that any accidental use of the upper bits would be conservative. In most ways it would be very similar to what we are doing now: we would still have to be careful in cases like a < b to mask out those Xes. But we would also have to do more to ensure that we were following this convention. For instance, by not caring about the upper bits, we don't have to do anything special when translating sums: the carry from a + b can go into the upper bits and it's just garbage. If we wanted all the upper bits to be X, we'd need to do extra work to mask them out in this case.

The other alternative seems sort of more proactive: we would essentially be fixing everything up to be the right size whether it needs to be fixed up or not. For instance, if we are translating something like (a + b) & c, we don't really need to know the true upper bits of a + b or c. We suspect that arranging for every expression to be correct out to infinite width would therefore incur some overhead.

Subtopics

Sv::vl-expr.lisp
Vttree
A data structure for collecting warnings and constraints while translating VL expressions to svex expressions.