hdl.ast: warn on unused property statements (Assert, Assume, etc).
A property statement that is created but not added to a module is virtually always a serious bug, since it can make formal verification pass when it should not. Therefore, add a warning to it, similar to UnusedElaboratable. Doing this to all statements is possible, but many temporary ones are created internally by nMigen, and the extensive changes required to remove false positives are likely not worth the true positives. We can revisit this in the future. Fixes #303.
This commit is contained in:
parent
9fb4a4f09e
commit
afece15001
|
@ -8,6 +8,7 @@ from enum import Enum
|
||||||
|
|
||||||
from .. import tracer
|
from .. import tracer
|
||||||
from .._utils import *
|
from .._utils import *
|
||||||
|
from .._unused import *
|
||||||
|
|
||||||
|
|
||||||
__all__ = [
|
__all__ = [
|
||||||
|
@ -17,9 +18,9 @@ __all__ = [
|
||||||
"Signal", "ClockSignal", "ResetSignal",
|
"Signal", "ClockSignal", "ResetSignal",
|
||||||
"UserValue",
|
"UserValue",
|
||||||
"Sample", "Past", "Stable", "Rose", "Fell", "Initial",
|
"Sample", "Past", "Stable", "Rose", "Fell", "Initial",
|
||||||
"Statement", "Assign", "Assert", "Assume", "Cover", "Switch",
|
"Statement", "Switch",
|
||||||
"ValueKey", "ValueDict", "ValueSet", "SignalKey", "SignalDict",
|
"Property", "Assign", "Assert", "Assume", "Cover",
|
||||||
"SignalSet",
|
"ValueKey", "ValueDict", "ValueSet", "SignalKey", "SignalDict", "SignalSet",
|
||||||
]
|
]
|
||||||
|
|
||||||
|
|
||||||
|
@ -493,13 +494,13 @@ class AnyValue(Value, DUID):
|
||||||
@final
|
@final
|
||||||
class AnyConst(AnyValue):
|
class AnyConst(AnyValue):
|
||||||
def __repr__(self):
|
def __repr__(self):
|
||||||
return "(anyconst {}'{})".format(self.nbits, "s" if self.signed else "")
|
return "(anyconst {}'{})".format(self.width, "s" if self.signed else "")
|
||||||
|
|
||||||
|
|
||||||
@final
|
@final
|
||||||
class AnySeq(AnyValue):
|
class AnySeq(AnyValue):
|
||||||
def __repr__(self):
|
def __repr__(self):
|
||||||
return "(anyseq {}'{})".format(self.nbits, "s" if self.signed else "")
|
return "(anyseq {}'{})".format(self.width, "s" if self.signed else "")
|
||||||
|
|
||||||
|
|
||||||
@final
|
@final
|
||||||
|
@ -1221,7 +1222,13 @@ class Assign(Statement):
|
||||||
return "(eq {!r} {!r})".format(self.lhs, self.rhs)
|
return "(eq {!r} {!r})".format(self.lhs, self.rhs)
|
||||||
|
|
||||||
|
|
||||||
class Property(Statement):
|
class UnusedProperty(UnusedMustUse):
|
||||||
|
pass
|
||||||
|
|
||||||
|
|
||||||
|
class Property(Statement, MustUse):
|
||||||
|
_MustUse__warning = UnusedProperty
|
||||||
|
|
||||||
def __init__(self, test, *, _check=None, _en=None, src_loc_at=0):
|
def __init__(self, test, *, _check=None, _en=None, src_loc_at=0):
|
||||||
super().__init__(src_loc_at=src_loc_at)
|
super().__init__(src_loc_at=src_loc_at)
|
||||||
self.test = Value.cast(test)
|
self.test = Value.cast(test)
|
||||||
|
|
|
@ -462,14 +462,16 @@ class Module(_ModuleBuilderRoot, Elaboratable):
|
||||||
while len(self._ctrl_stack) > self.domain._depth:
|
while len(self._ctrl_stack) > self.domain._depth:
|
||||||
self._pop_ctrl()
|
self._pop_ctrl()
|
||||||
|
|
||||||
for assign in Statement.cast(assigns):
|
for stmt in Statement.cast(assigns):
|
||||||
if not compat_mode and not isinstance(assign, (Assign, Assert, Assume, Cover)):
|
if not compat_mode and not isinstance(stmt, (Assign, Assert, Assume, Cover)):
|
||||||
raise SyntaxError(
|
raise SyntaxError(
|
||||||
"Only assignments and property checks may be appended to d.{}"
|
"Only assignments and property checks may be appended to d.{}"
|
||||||
.format(domain_name(domain)))
|
.format(domain_name(domain)))
|
||||||
|
|
||||||
assign = SampleDomainInjector(domain)(assign)
|
stmt._MustUse__used = True
|
||||||
for signal in assign._lhs_signals():
|
stmt = SampleDomainInjector(domain)(stmt)
|
||||||
|
|
||||||
|
for signal in stmt._lhs_signals():
|
||||||
if signal not in self._driving:
|
if signal not in self._driving:
|
||||||
self._driving[signal] = domain
|
self._driving[signal] = domain
|
||||||
elif self._driving[signal] != domain:
|
elif self._driving[signal] != domain:
|
||||||
|
@ -479,7 +481,7 @@ class Module(_ModuleBuilderRoot, Elaboratable):
|
||||||
"already driven from d.{}"
|
"already driven from d.{}"
|
||||||
.format(signal, domain_name(domain), domain_name(cd_curr)))
|
.format(signal, domain_name(domain), domain_name(cd_curr)))
|
||||||
|
|
||||||
self._statements.append(assign)
|
self._statements.append(stmt)
|
||||||
|
|
||||||
def _add_submodule(self, submodule, name=None):
|
def _add_submodule(self, submodule, name=None):
|
||||||
if not hasattr(submodule, "elaborate"):
|
if not hasattr(submodule, "elaborate"):
|
||||||
|
|
|
@ -121,7 +121,9 @@ class Fragment:
|
||||||
yield from self.domains
|
yield from self.domains
|
||||||
|
|
||||||
def add_statements(self, *stmts):
|
def add_statements(self, *stmts):
|
||||||
self.statements += Statement.cast(stmts)
|
for stmt in Statement.cast(stmts):
|
||||||
|
stmt._MustUse__used = True
|
||||||
|
self.statements.append(stmt)
|
||||||
|
|
||||||
def add_subfragment(self, subfragment, name=None):
|
def add_subfragment(self, subfragment, name=None):
|
||||||
assert isinstance(subfragment, Fragment)
|
assert isinstance(subfragment, Fragment)
|
||||||
|
|
|
@ -234,6 +234,8 @@ class StatementVisitor(metaclass=ABCMeta):
|
||||||
new_stmt.src_loc = stmt.src_loc
|
new_stmt.src_loc = stmt.src_loc
|
||||||
if isinstance(new_stmt, Switch) and isinstance(stmt, Switch):
|
if isinstance(new_stmt, Switch) and isinstance(stmt, Switch):
|
||||||
new_stmt.case_src_locs = stmt.case_src_locs
|
new_stmt.case_src_locs = stmt.case_src_locs
|
||||||
|
if isinstance(new_stmt, Property):
|
||||||
|
new_stmt._MustUse__used = True
|
||||||
return new_stmt
|
return new_stmt
|
||||||
|
|
||||||
def __call__(self, stmt):
|
def __call__(self, stmt):
|
||||||
|
|
Loading…
Reference in a new issue