hdl.ast: implement Initial.

This is the last remaining part for first-class formal support.

diff --git a/nmigen/back/pysim.py b/nmigen/back/pysim.py
index e88972cbcdfa0af37fa655fe562de9db73a87e57..93329c4c2480d07fbc9bcc9b03f33975cbec65db 100644 (file)
--- a/nmigen/back/pysim.py
+++ b/nmigen/back/pysim.py
@@ -86,6 +86,9 @@ class _ValueCompiler(ValueVisitor):
     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()))
 

diff --git a/nmigen/back/rtlil.py b/nmigen/back/rtlil.py
index ac2b99fc0d9dc4d0c08fcdcc4b60bd730695fe26..3c4da8b3ba9315f543b5a49adc6250c8a157ff38 100644 (file)
--- a/nmigen/back/rtlil.py
+++ b/nmigen/back/rtlil.py
@@ -331,6 +331,9 @@ class _ValueCompiler(xfrm.ValueVisitor):
     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()))
 

diff --git a/nmigen/formal.py b/nmigen/formal.py
index 2836cca077c1203d57664e0597d58c972f43a009..f374cf0e296cad14cbc07ba0747283e586f90494 100644 (file)
--- a/nmigen/formal.py
+++ b/nmigen/formal.py
@@ -1,2 +1,2 @@
 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

diff --git a/nmigen/hdl/ast.py b/nmigen/hdl/ast.py
index 749b8a29b4142f79d4c804cc8f294602f1b3399a..757f5268d26256ce6bb3b7a11e82dbf8ddc7655d 100644 (file)
--- a/nmigen/hdl/ast.py
+++ b/nmigen/hdl/ast.py
@@ -12,9 +12,9 @@ from ..tools import *
 __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",
@@ -957,7 +957,7 @@ class Sample(Value):
         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:
@@ -991,6 +991,25 @@ def Fell(expr, clocks=0, domain=None):
     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)))
@@ -1276,6 +1295,8 @@ class ValueKey:
                               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))
@@ -1322,6 +1343,8 @@ class ValueKey:
             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))

diff --git a/nmigen/hdl/xfrm.py b/nmigen/hdl/xfrm.py
index 921bcaee5c801b22c0698c62d0f3baafe869d394..11bfd2a7a1ab3494c233e6ee4133207a77674e29 100644 (file)
--- a/nmigen/hdl/xfrm.py
+++ b/nmigen/hdl/xfrm.py
@@ -78,6 +78,10 @@ class ValueVisitor(metaclass=ABCMeta):
     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:
 
@@ -115,6 +119,8 @@ class ValueVisitor(metaclass=ABCMeta):
             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())
@@ -173,6 +179,9 @@ class ValueTransformer(ValueVisitor):
     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
@@ -371,6 +380,9 @@ class DomainCollector(ValueVisitor, StatementVisitor):
     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)
@@ -491,6 +503,7 @@ class SampleDomainInjector(ValueTransformer, StatementTransformer):
 
 class SampleLowerer(FragmentTransformer, ValueTransformer, StatementTransformer):
     def __init__(self):
+        self.initial = None
         self.sample_cache = None
         self.sample_stmts = None
 
@@ -503,6 +516,8 @@ class SampleLowerer(FragmentTransformer, ValueTransformer, StatementTransformer)
             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:
 
@@ -510,8 +525,9 @@ class SampleLowerer(FragmentTransformer, ValueTransformer, StatementTransformer)
         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)
@@ -519,7 +535,7 @@ class SampleLowerer(FragmentTransformer, ValueTransformer, StatementTransformer)
             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))
@@ -527,7 +543,13 @@ class SampleLowerer(FragmentTransformer, ValueTransformer, StatementTransformer)
         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))
@@ -535,6 +557,8 @@ class SampleLowerer(FragmentTransformer, ValueTransformer, StatementTransformer)
             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):

diff --git a/nmigen/lib/fifo.py b/nmigen/lib/fifo.py
index 386d9031fc6fae517e3f6fb0ebf5b38ca3648fbf..c59a040c13c4f88c1b969169b2593ac285bfb3c7 100644 (file)
--- a/nmigen/lib/fifo.py
+++ b/nmigen/lib/fifo.py
@@ -181,9 +181,7 @@ class SyncFIFO(Elaboratable, FIFOInterface):
 
         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),
@@ -351,10 +349,7 @@ class AsyncFIFO(Elaboratable, FIFOInterface):
         ]
 
         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:]))
 

diff --git a/nmigen/test/test_hdl_ast.py b/nmigen/test/test_hdl_ast.py
index 6fa0a1cbd7d21a48afd67a803105ba797690ef9d..c9688ee541491141d72d4fb1d08eba8f406b81f5 100644 (file)
--- a/nmigen/test/test_hdl_ast.py
+++ b/nmigen/test/test_hdl_ast.py
@@ -614,3 +614,9 @@ class SampleTestCase(FHDLTestCase):
         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))

diff --git a/nmigen/test/test_lib_fifo.py b/nmigen/test/test_lib_fifo.py
index d6ce220da432828b78249d978d2bd4ca5bdc0e6e..9176037f6744d617d1be8ade2c082246efe413b7 100644 (file)
--- a/nmigen/test/test_lib_fifo.py
+++ b/nmigen/test/test_lib_fifo.py
@@ -208,12 +208,10 @@ class FIFOContractSpec(Elaboratable):
                 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":