From b6cff2c0987d19495b706cc586d3c1606e6aff76 Mon Sep 17 00:00:00 2001
From: whitequark <whitequark@whitequark.org>
Date: Sun, 20 Jan 2019 02:20:34 +0000
Subject: [PATCH] lib.coding: add GrayEncoder and GrayDecoder.

Unlike the Migen ones, these are purely combinatorial.
---
 nmigen/lib/coding.py           | 63 ++++++++++++++++++++++++++++++++++
 nmigen/test/test_lib_coding.py | 45 ++++++++++++++++++++++++
 2 files changed, 108 insertions(+)

diff --git a/nmigen/lib/coding.py b/nmigen/lib/coding.py
index 081858b..653882f 100644
--- a/nmigen/lib/coding.py
+++ b/nmigen/lib/coding.py
@@ -3,6 +3,13 @@
 from .. import *
 
 
+__all__ = [
+    "Encoder", "Decoder",
+    "PriorityEncoder", "PriorityDecoder",
+    "GrayEncoder", "GrayDecoder",
+]
+
+
 class Encoder:
     """Encode one-hot to binary.
 
@@ -121,3 +128,59 @@ class PriorityDecoder(Decoder):
 
     Identical to :class:`Decoder`.
     """
+
+
+class GrayEncoder:
+    """Encode binary to Gray code.
+
+    Parameters
+    ----------
+    width : int
+        Bit width.
+
+    Attributes
+    ----------
+    i : Signal(width), in
+        Input natural binary.
+    o : Signal(width), out
+        Encoded Gray code.
+    """
+    def __init__(self, width):
+        self.width = width
+
+        self.i = Signal(width)
+        self.o = Signal(width)
+
+    def get_fragment(self, platform):
+        m = Module()
+        m.d.comb += self.o.eq(self.i ^ self.i[1:])
+        return m.lower(platform)
+
+
+class GrayDecoder:
+    """Decode Gray code to binary.
+
+    Parameters
+    ----------
+    width : int
+        Bit width.
+
+    Attributes
+    ----------
+    i : Signal(width), in
+        Input Gray code.
+    o : Signal(width), out
+        Decoded natural binary.
+    """
+    def __init__(self, width):
+        self.width = width
+
+        self.i = Signal(width)
+        self.o = Signal(width)
+
+    def get_fragment(self, platform):
+        m = Module()
+        m.d.comb += self.o[-1].eq(self.i[-1])
+        for i in reversed(range(self.width - 1)):
+            m.d.comb += self.o[i].eq(self.o[i + 1] ^ self.i[i])
+        return m.lower(platform)
diff --git a/nmigen/test/test_lib_coding.py b/nmigen/test/test_lib_coding.py
index c535c79..53f2b8b 100644
--- a/nmigen/test/test_lib_coding.py
+++ b/nmigen/test/test_lib_coding.py
@@ -1,5 +1,6 @@
 from .tools import *
 from ..hdl.ast import *
+from ..hdl.dsl import *
 from ..back.pysim import *
 from ..lib.coding import *
 
@@ -79,3 +80,47 @@ class DecoderTestCase(FHDLTestCase):
 
             sim.add_process(process)
             sim.run()
+
+
+class ReversibleSpec:
+    def __init__(self, encoder_cls, decoder_cls, args):
+        self.encoder_cls = encoder_cls
+        self.decoder_cls = decoder_cls
+        self.coder_args  = args
+
+    def get_fragment(self, platform):
+        m = Module()
+        enc, dec = self.encoder_cls(*self.coder_args), self.decoder_cls(*self.coder_args)
+        m.submodules += enc, dec
+        m.d.comb += [
+            dec.i.eq(enc.o),
+            Assert(enc.i == dec.o)
+        ]
+        return m.lower(platform)
+
+
+class HammingDistanceSpec:
+    def __init__(self, distance, encoder_cls, args):
+        self.distance    = distance
+        self.encoder_cls = encoder_cls
+        self.coder_args  = args
+
+    def get_fragment(self, platform):
+        m = Module()
+        enc1, enc2 = self.encoder_cls(*self.coder_args), self.encoder_cls(*self.coder_args)
+        m.submodules += enc1, enc2
+        m.d.comb += [
+            Assume(enc1.i + 1 == enc2.i),
+            Assert(sum(enc1.o ^ enc2.o) == self.distance)
+        ]
+        return m.lower(platform)
+
+
+class GrayCoderTestCase(FHDLTestCase):
+    def test_reversible(self):
+        spec = ReversibleSpec(encoder_cls=GrayEncoder, decoder_cls=GrayDecoder, args=(16,))
+        self.assertFormal(spec, mode="prove")
+
+    def test_distance(self):
+        spec = HammingDistanceSpec(distance=1, encoder_cls=GrayEncoder, args=(16,))
+        self.assertFormal(spec, mode="prove")
-- 
2.30.2