From: whitequark <whitequark@whitequark.org>
Date: Sat, 19 Jan 2019 06:02:04 +0000 (+0000)
Subject: hdl.xfrm: mark internal registers used in lowering Sample().
X-Git-Tag: working~62
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c5d67b0461714c499347ad255d2cc974632a62e9;p=nmigen.git

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

diff --git a/nmigen/hdl/xfrm.py b/nmigen/hdl/xfrm.py
index ca43cf5..e5f415e 100644
--- 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 ba938ba..16d19de 100644
--- 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 e34f310..a995162 100644
--- 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 = ""