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

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:

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)
 

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 = ""