hdl.xfrm: mark internal registers used in lowering Sample().

diff --git a/nmigen/hdl/xfrm.py b/nmigen/hdl/xfrm.py
index ca43cf5fdfce483b9d2c65e4a2ff88d229b2adfa..e5f415e9e710e7adb2b7ba758891f560147bae9c 100644 (file)
--- a/nmigen/hdl/xfrm.py
+++ b/nmigen/hdl/xfrm.py
@@ -385,6 +385,7 @@ class SampleLowerer(FragmentTransformer, ValueTransformer, StatementTransformer)
             sampled_name, sampled_reset = self._name_reset(value.value)
             name = "$sample${}${}${}".format(sampled_name, value.domain, value.clocks)
             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))
             if value.domain not in self.sample_stmts:

diff --git a/nmigen/test/test_lib_fifo.py b/nmigen/test/test_lib_fifo.py
index ba938bac77cac16e3f8be37e1e2f88295664ccf5..16d19de05d29c7022b9fa9583d9e3651cf27471a 100644 (file)
--- a/nmigen/test/test_lib_fifo.py
+++ b/nmigen/test/test_lib_fifo.py
@@ -78,17 +78,13 @@ class FIFOContract:
                 with m.If((read_1 == entry_1) & (read_2 == entry_2)):
                     m.next = "DONE"
 
-        cycle = Signal(max=self.bound + 1, reset=1)
-        m.d.sync += cycle.eq(cycle + 1)
-        with m.If(cycle == self.bound):
-            m.d.comb += Assert(read_fsm.ongoing("DONE"))
-
         initstate = Signal()
         m.submodules += Instance("$initstate", o_Y=initstate)
         with m.If(initstate):
             m.d.comb += Assume(write_fsm.ongoing("WRITE-1"))
             m.d.comb += Assume(read_fsm.ongoing("READ"))
-            m.d.comb += Assume(cycle == 1)
+        with m.If(Past(initstate, self.bound - 1)):
+            m.d.comb += Assert(read_fsm.ongoing("DONE"))
 
         return m.lower(platform)
 

diff --git a/nmigen/test/tools.py b/nmigen/test/tools.py
index e34f31081be08aa21a17f1be587f54f0aaa673c2..a995162ba4467d970ab919c507ad0260468014ac 100644 (file)
--- a/nmigen/test/tools.py
+++ b/nmigen/test/tools.py
@@ -65,7 +65,7 @@ class FHDLTestCase(unittest.TestCase):
 
         if mode == "hybrid":
             # A mix of BMC and k-induction, as per personal communication with Clifford Wolf.
-            script = "setattr -unset init w:*"
+            script = "setattr -unset init w:* a:nmigen.sample_reg %d"
             mode   = "bmc"
         else:
             script = ""