# Disable pylint's "your name is too short" warning.
# pylint: disable=C0103
from typing import List, Tuple

from amaranth import Signal, Module, Elaboratable
from amaranth.build import Platform
from amaranth.asserts import Assume, Assert, Cover

from util import main


class CoinCounter(Elaboratable):
    """Logic for my module.

    This is a skeleton for writing your own modules.
    """

    def __init__(self):
        # Inputs
        self.pennies_in = Signal(8)
        self.nickels_in = Signal(4)
        self.dimes_in = Signal(4)
        self.quarters_in = Signal(4)
        self.dollars_in = Signal(4)

        # Outputs
        self.pennies_out = Signal(16)

    def elaborate(self, _: Platform) -> Module:
        """Implements the logic for my module."""
        m = Module()

        m.d.comb += self.pennies_out.eq(
                self.pennies_in + 5 * self.nickels_in +
                10 * self.dimes_in + 25 * self.quarters_in +
                100 * self.dollars_in)

        return m

    @classmethod
    def formal(cls) -> Tuple[Module, List[Signal]]:
        """Formal verification for my module."""
        m = Module()
        m.submodules.my_class = my_class = cls()

        # Make sure that the output is always the same as the input
        m.d.comb += Assert((my_class.pennies_out % 5) == (my_class.pennies_in % 5))

        # Cover the case where the output is 1.
        # m.d.comb += Cover(my_class.my_output == 1)

        return m, [my_class.pennies_in, my_class.nickels_in, my_class.dimes_in, my_class.quarters_in, my_class.dollars_in]


if __name__ == "__main__":
    main(CoinCounter)