• 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
          • Trunc
          • Always-top
            • Edgesynth
            • Stmtrewrite
            • Cblock
              • Vl-stmt-cblock-p
              • Cblock-path-checking
                • Vl-modulelist-combinational-elim
                • Vl-always-check-cblock
                • Vl-filter-cblocks
                • Vl-check-sensitivity-list
                • Vl-atomicstmt-cblock-varexpr
                • Vl-cblock-synth
                • Vl-cblock-make-assign
                • Vl-module-combinational-elim
                • Vl-cblocks-synth
                • Vl-cblock-make-assigns
                • Vl-cblock-pathcheck
                • Vl-atomicstmt-cblock-pathcheck1
                • Vl-stmt-cblock-varexpr
                • Vl-design-combinational-elim
                • Vl-stmtlist-cblock-pathcheck1
                • Vl-stmt-cblock-pathcheck1
              • Cblock-expression-building
              • Vl-stmt-cblock-lvalexprs
              • Vl-stmt-cblock-rvalexprs
              • Vl-classic-control->exprs
              • Vl-classic-control-p
              • Vl-star-control-p
            • Vl-always-convert-regports
            • Vl-always-convert-regs
            • Stmttemps
            • Edgesplit
            • Vl-always-check-reg
            • Vl-convert-regs
            • Latchsynth
            • Vl-always-check-regs
            • Vl-match-always-at-some-edges
            • Unelse
            • Vl-always-convert-reg
            • Vl-design-always-backend
            • Vl-stmt-guts
            • Vl-always-convert-regport
            • Vl-always-scary-regs
            • Eliminitial
            • Ifmerge
            • Vl-edge-control-p
            • Elimalways
          • 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
  • Cblock

Cblock-path-checking

How we check whether all of the variables assigned to in an always block are, indeed, assigned to in all paths. In other words: how we know that we don't need to infer a latch.

This is a basic criteria for whether we can treat an always block as combinational. Some examples of what we want to accept and reject:

always @(*)                        <---- OK, combinational block because
  if (c1) lhs = rhs1;                    LHS is assigned in every branch.
  else lhs = rhs2;

always @(*)                        <---- NOT OK, need to infer a latch
  if (c1) lhs = rhs;                     because LHS must hold its value
                                         when C1 is false.

always @(*)                        <---- OK, combinational block because
  lhs = rhs1;                            LHS is assigned in every branch.
  if (c1) lhs = rhs2;

Our implementation is brain-dead simple: we write a function that checks whether a particular LHS is assigned in every branch. Then we'll apply that function to every LHS that is used anywhere in the block.

This approach fails to identify "arguably" combinational always blocks such as:

always @(*)
  if (c1) lhs = rhs1;
  if (!c1) lhs = rhs2;

because our path exploration function stupidly does not consider the possible relationships between the conditions.

Well, it's not clear that we should try to do anything smarter than this. After all, synthesis tools might not do hard work here, either.

Subtopics

Vl-modulelist-combinational-elim
(vl-modulelist-combinational-elim x) maps vl-module-combinational-elim across a list.
Vl-always-check-cblock
Check whether an always block looks like a combinational block that we can support.
Vl-filter-cblocks
Separate always blocks into supported combinational blocks and others.
Vl-check-sensitivity-list
Check if the sensitivity list is okay for a combinational block.
Vl-atomicstmt-cblock-varexpr
Update our current expression for varname to account for a new atomic statement.
Vl-cblock-synth
Should only be called on good cblocks.
Vl-cblock-make-assign
Vl-module-combinational-elim
Vl-cblocks-synth
Vl-cblock-make-assigns
Vl-cblock-pathcheck
Check whether a list of variables are always assigned to in every execution of the always block, i.e., whether this really is a purely combinational block.
Vl-atomicstmt-cblock-pathcheck1
Vl-stmt-cblock-varexpr
Construct the expression for a single variable.
Vl-design-combinational-elim
Vl-stmtlist-cblock-pathcheck1
Check that a single variable is always assigned to, in all paths, within some statement in a begin/end block list.
Vl-stmt-cblock-pathcheck1
Check that a single variable is assigned to in all branches of this statement.