• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
      • Vl2014
        • Warnings
        • Primitives
        • Use-set
        • Syntax
        • Getting-started
        • Utilities
        • Loader
        • Transforms
          • Expression-sizing
          • Occform
          • Oprewrite
          • Expand-functions
          • Delayredux
          • Unparameterization
          • Caseelim
          • Split
          • Selresolve
          • Weirdint-elim
          • Vl-delta
          • Replicate-insts
          • Rangeresolve
          • Propagate
          • Clean-selects
          • Clean-params
          • Blankargs
          • Inline-mods
          • Expr-simp
            • Vl-plainarglist-simp
            • Vl-modinstlist-simp
            • Vl-modulelist-simp
            • Vl-assignlist-simp
            • Vl-expr-simp-unary-bitnot
            • Vl-expr-simp-binary-bitor
            • Vl-expr-simp-binary-bitand
            • Vl-expr-simp-qmark
            • Vl-modinst-simp
            • Vl-plainarg-simp
            • Vl-module-simp
            • Vl-design-simp
            • Vl-assign-simp
            • Vl-expr-simp
          • Trunc
          • Always-top
          • Gatesplit
          • Gate-elim
          • Expression-optimization
          • Elim-supplies
          • Wildelim
          • Drop-blankports
          • Clean-warnings
          • Addinstnames
          • Custom-transform-hooks
          • Annotate
          • Latchcode
          • Elim-unused-vars
          • Problem-modules
        • Lint
        • Mlib
        • Server
        • Kit
        • Printer
        • Esim-vl
        • Well-formedness
      • Sv
      • Fgl
      • Vwsim
      • Vl
      • X86isa
      • Svl
      • Rtl
    • Software-verification
    • Math
    • Testing-utilities
  • Transforms

Expr-simp

Carry out basic expression simplification. (UNSOUND)

This transform does a lot of basic rewriting of expressions, e.g., it will eliminate double negations, propagate constants through ANDs, use Demorgan's rule to simplify negated ANDs, pushing nots down into the branches of ?: expressions, and so forth.

WARNING: These transforms are almost certainly unsound in general. For instance, even something as simple as removing double negatives isn't stricly correct, ~~A will produce X when A is Z. On the other hand, these rewrites are probably okay if we only care about the Boolean values of expressions.

BUT FOR SERIOUSLY -- WARNING: I am really not too concerned with soundness here. There are probably many things that could go wrong w.r.t. expression sizes, etc. You should check that this produces reasonable output using an equivalence checker.

Subtopics

Vl-plainarglist-simp
(vl-plainarglist-simp x) maps vl-plainarg-simp across a list.
Vl-modinstlist-simp
(vl-modinstlist-simp x) maps vl-modinst-simp across a list.
Vl-modulelist-simp
(vl-modulelist-simp x) maps vl-module-simp across a list.
Vl-assignlist-simp
(vl-assignlist-simp x) maps vl-assign-simp across a list.
Vl-expr-simp-unary-bitnot
Vl-expr-simp-binary-bitor
Vl-expr-simp-binary-bitand
Vl-expr-simp-qmark
Vl-modinst-simp
Vl-plainarg-simp
Vl-module-simp
Vl-design-simp
Top-level expr-simp transform.
Vl-assign-simp
Vl-expr-simp
Core routine to simplify expressions.