search

dz333 / secverilog

4 stars 0 forks source link

Add unassigned path check for sequential variables #15

Closed dz333 closed 1 year ago

dz333 commented 1 year ago

For all sequential variables with a dependent type, v,

If there are any paths on which v is not assigned, then we must check that L(v) flows to L(next v) on that path.

For example, if our path analysis for v says [ v -> { a, !b, c && d } ] then we want to check:

if !(a or !b or (c && d)) then L(v) f.t. L(next v)

dz333 commented 1 year ago

Completed!