This is the last remaining part for first-class formal support.
def on_Sample(self, value):
raise NotImplementedError # :nocov:
+ def on_Initial(self, value):
+ raise NotImplementedError # :nocov:
+
def on_Record(self, value):
return self(Cat(value.fields.values()))
def on_Sample(self, value):
raise NotImplementedError # :nocov:
+ def on_Initial(self, value):
+ raise NotImplementedError # :nocov:
+
def on_Record(self, value):
return self(ast.Cat(value.fields.values()))
from .hdl.ast import AnyConst, AnySeq, Assert, Assume
-from .hdl.ast import Past, Stable, Rose, Fell
+from .hdl.ast import Past, Stable, Rose, Fell, Initial
__all__ = [
"Value", "Const", "C", "AnyConst", "AnySeq", "Operator", "Mux", "Part", "Slice", "Cat", "Repl",
"Array", "ArrayProxy",
- "Sample", "Past", "Stable", "Rose", "Fell",
"Signal", "ClockSignal", "ResetSignal",
"UserValue",
+ "Sample", "Past", "Stable", "Rose", "Fell", "Initial",
"Statement", "Assign", "Assert", "Assume", "Switch", "Delay", "Tick",
"Passive", "ValueKey", "ValueDict", "ValueSet", "SignalKey", "SignalDict",
"SignalSet",
self.value = Value.wrap(expr)
self.clocks = int(clocks)
self.domain = domain
- if not isinstance(self.value, (Const, Signal, ClockSignal, ResetSignal)):
+ if not isinstance(self.value, (Const, Signal, ClockSignal, ResetSignal, Initial)):
raise TypeError("Sampled value may only be a signal or a constant, not {!r}"
.format(self.value))
if self.clocks < 0:
return Sample(expr, clocks + 1, domain) & ~Sample(expr, clocks, domain)
+@final
+class Initial(Value):
+ """Start indicator, for formal verification.
+
+ An ``Initial`` signal is ``1`` at the first cycle of model checking, and ``0`` at any other.
+ """
+ def __init__(self, *, src_loc_at=0):
+ super().__init__(src_loc_at=1 + src_loc_at)
+
+ def shape(self):
+ return (1, False)
+
+ def _rhs_signals(self):
+ return ValueSet((self,))
+
+ def __repr__(self):
+ return "(initial)"
+
+
class _StatementList(list):
def __repr__(self):
return "({})".format(" ".join(map(repr, self)))
tuple(ValueKey(e) for e in self.value._iter_as_values())))
elif isinstance(self.value, Sample):
self._hash = hash((ValueKey(self.value.value), self.value.clocks, self.value.domain))
+ elif isinstance(self.value, Initial):
+ self._hash = 0
else: # :nocov:
raise TypeError("Object '{!r}' cannot be used as a key in value collections"
.format(self.value))
return (ValueKey(self.value.value) == ValueKey(other.value.value) and
self.value.clocks == other.value.clocks and
self.value.domain == self.value.domain)
+ elif isinstance(self.value, Initial):
+ return True
else: # :nocov:
raise TypeError("Object '{!r}' cannot be used as a key in value collections"
.format(self.value))
def on_Sample(self, value):
pass # :nocov:
+ @abstractmethod
+ def on_Initial(self, value):
+ pass # :nocov:
+
def on_unknown_value(self, value):
raise TypeError("Cannot transform value '{!r}'".format(value)) # :nocov:
new_value = self.on_ArrayProxy(value)
elif type(value) is Sample:
new_value = self.on_Sample(value)
+ elif type(value) is Initial:
+ new_value = self.on_Initial(value)
elif isinstance(value, UserValue):
# Uses `isinstance()` and not `type() is` to allow inheriting.
new_value = self.on_value(value._lazy_lower())
def on_Sample(self, value):
return Sample(self.on_value(value.value), value.clocks, value.domain)
+ def on_Initial(self, value):
+ return value
+
class StatementVisitor(metaclass=ABCMeta):
@abstractmethod
def on_Sample(self, value):
self.on_value(value.value)
+ def on_Initial(self, value):
+ pass
+
def on_Assign(self, stmt):
self.on_value(stmt.lhs)
self.on_value(stmt.rhs)
class SampleLowerer(FragmentTransformer, ValueTransformer, StatementTransformer):
def __init__(self):
+ self.initial = None
self.sample_cache = None
self.sample_stmts = None
return "clk", 0
elif isinstance(value, ResetSignal):
return "rst", 1
+ elif isinstance(value, Initial):
+ return "init", 0 # Past(Initial()) produces 0, 1, 0, 0, ...
else:
raise NotImplementedError # :nocov:
if value in self.sample_cache:
return self.sample_cache[value]
+ sampled_value = self.on_value(value.value)
if value.clocks == 0:
- sample = value.value
+ sample = sampled_value
else:
assert value.domain is not None
sampled_name, sampled_reset = self._name_reset(value.value)
sample = Signal.like(value.value, name=name, reset_less=True, reset=sampled_reset)
sample.attrs["nmigen.sample_reg"] = True
- prev_sample = self.on_Sample(Sample(value.value, value.clocks - 1, value.domain))
+ prev_sample = self.on_Sample(Sample(sampled_value, value.clocks - 1, value.domain))
if value.domain not in self.sample_stmts:
self.sample_stmts[value.domain] = []
self.sample_stmts[value.domain].append(sample.eq(prev_sample))
self.sample_cache[value] = sample
return sample
+ def on_Initial(self, value):
+ if self.initial is None:
+ self.initial = Signal(name="init")
+ return self.initial
+
def map_statements(self, fragment, new_fragment):
+ self.initial = None
self.sample_cache = ValueDict()
self.sample_stmts = OrderedDict()
new_fragment.add_statements(map(self.on_statement, fragment.statements))
new_fragment.add_statements(stmts)
for stmt in stmts:
new_fragment.add_driver(stmt.lhs, domain)
+ if self.initial is not None:
+ new_fragment.add_subfragment(Instance("$initstate", o_Y=self.initial))
class SwitchCleaner(StatementVisitor):
if platform == "formal":
# TODO: move this logic to SymbiYosys
- initstate = Signal()
- m.submodules += Instance("$initstate", o_Y=initstate)
- with m.If(initstate):
+ with m.If(Initial()):
m.d.comb += [
Assume(produce < self.depth),
Assume(consume < self.depth),
]
if platform == "formal":
- # TODO: move this logic elsewhere
- initstate = Signal()
- m.submodules += Instance("$initstate", o_Y=initstate)
- with m.If(initstate):
+ with m.If(Initial()):
m.d.comb += Assume(produce_w_gry == (produce_w_bin ^ produce_w_bin[1:]))
m.d.comb += Assume(consume_r_gry == (consume_r_bin ^ consume_r_bin[1:]))
with self.assertRaises(ValueError,
"Cannot sample a value 1 cycles in the future"):
Sample(Signal(), -1, "sync")
+
+
+class InitialTestCase(FHDLTestCase):
+ def test_initial(self):
+ i = Initial()
+ self.assertEqual(i.shape(), (1, False))
with m.If((read_1 == entry_1) & (read_2 == entry_2)):
m.next = "DONE"
- initstate = Signal()
- m.submodules += Instance("$initstate", o_Y=initstate)
- with m.If(initstate):
+ with m.If(Initial()):
m.d.comb += Assume(write_fsm.ongoing("WRITE-1"))
m.d.comb += Assume(read_fsm.ongoing("READ"))
- with m.If(Past(initstate, self.bound - 1)):
+ with m.If(Past(Initial(), self.bound - 1)):
m.d.comb += Assert(read_fsm.ongoing("DONE"))
if self.wdomain != "sync" or self.rdomain != "sync":
projects / nmigen.git / commitdiff