mc14500.py

from enum import Enum
from nmigen import *
from nmigen.asserts import *
from nmigen.sim import pysim

class Opcodes(Enum):
    NOPO = 0x0
    LD = 0x1
    LDC = 0x2
    AND = 0x3
    ANDC = 0x4
    OR = 0x5
    ORC = 0x6
    XNOR = 0x7
    STO = 0x8
    STOC = 0x9
    IEN = 0xA
    OEN = 0xB
    JMP = 0xC
    RTN = 0xD
    SKZ = 0xE
    NOPF = 0xF

class MC14500(Elaboratable):
    def __init__(self):
        self.write = Signal()
        self.data_i = Signal()
        self.data_o = Signal()
        
        self.i = Signal(4, decoder=Opcodes)

        self.flag_f = Signal()
        self.flag_o = Signal()
        self.rtn = Signal()
        self.jmp = Signal()

        self.rr = Signal()
    
    def elaborate(self, platform):
        m = Module()

        ien = Signal()
        oen = Signal()
        rr = Signal()

        # Input data is gated by the IEN register
        data_i = Signal()
        m.d.comb += data_i.eq(self.data_i & ien)

        # Write signal is gated by the OEN register
        write = Signal()
        m.d.comb += self.write.eq(write & oen)

        skip = Signal()

        # Only last one clock cycle
        m.d.sync += [
            self.flag_f.eq(0),
            self.flag_o.eq(0),
            self.rtn.eq(0),
            self.jmp.eq(0),

            skip.eq(0)
        ]

        with m.If(~skip):
            with m.Switch(self.i):
                with m.Case(Opcodes.NOPO):
                    m.d.sync += self.flag_o.eq(1)
                with m.Case(Opcodes.LD):
                    m.d.sync += rr.eq(data_i)
                with m.Case(Opcodes.LDC):
                    m.d.sync += rr.eq(~data_i)
                with m.Case(Opcodes.AND):
                    m.d.sync += rr.eq(rr & data_i)
                with m.Case(Opcodes.ANDC):
                    m.d.sync += rr.eq(rr & ~data_i)
                with m.Case(Opcodes.OR):
                    m.d.sync += rr.eq(rr | data_i)
                with m.Case(Opcodes.ORC):
                    m.d.sync += rr.eq(rr | ~data_i)
                with m.Case(Opcodes.XNOR):
                    m.d.sync += rr.eq(~(rr ^ data_i))
                with m.Case(Opcodes.STO):
                    m.d.comb += [
                        write.eq(1),
                        self.data_o.eq(rr)
                    ]
                with m.Case(Opcodes.STOC):
                    m.d.comb += [
                        write.eq(1),
                        self.data_o.eq(~rr)
                    ]
                with m.Case(Opcodes.IEN):
                    m.d.sync += ien.eq(self.data_i)
                with m.Case(Opcodes.OEN):
                    m.d.sync += oen.eq(self.data_i)
                with m.Case(Opcodes.JMP):
                    m.d.sync += self.jmp.eq(1)
                with m.Case(Opcodes.RTN):
                    m.d.sync += self.rtn.eq(1)
                with m.Case(Opcodes.SKZ):
                    with m.If(~rr):
                        m.d.sync += skip.eq(1)
                    with m.Else():
                        m.d.sync += skip.eq(0)
                with m.Case(Opcodes.NOPF):
                    m.d.sync += self.flag_f.eq(1)

        if platform == "formal":
            m.d.comb += Assume(~ResetSignal(domain='sync'))

            single_cycle_flags = [
                (Opcodes.NOPO, self.flag_o),
                (Opcodes.JMP, self.jmp),
                (Opcodes.RTN, self.rtn),
                (Opcodes.NOPF, self.flag_f)
            ]
            for opcode, flag in single_cycle_flags:
                with m.If(Past(flag) & (Past(self.i) != opcode)):
                    m.d.sync += Assert(Fell(flag))
                with m.If(~Initial() & (Past(self.i) == opcode) & ~Past(skip)):
                    m.d.sync += Assert(flag | Rose(flag))

            rr_stable = [
                Opcodes.NOPO,
                Opcodes.STO,
                Opcodes.STOC,
                Opcodes.IEN,
                Opcodes.OEN,
                Opcodes.JMP,
                Opcodes.RTN,
                Opcodes.SKZ,
                Opcodes.NOPF
            ]
            for opcode in rr_stable:
                with m.If(~Initial() & (Past(self.i) == opcode)):
                    m.d.sync += Assert(Stable(rr))

            with m.If(~oen):
                m.d.comb += Assert(~self.write)

        return m

import unittest
class MC14500TestCase(unittest.TestCase):
    def do_sim(self, uut, proc, vcd_file=None):
        sim = pysim.Simulator(uut)
        sim.add_clock(1e-9)
        sim.add_sync_process(proc)

        if vcd_file is not None:
            with sim.write_vcd(vcd_file):
                sim.run()
        else:
            sim.run()

    def test_single_cycle_flags(self):
        en = Signal()
        uut = EnableInserter(en)(MC14500())

        def proc():
            self.assertEqual((yield uut.flag_f), 0)
            self.assertEqual((yield uut.flag_o), 0)
            self.assertEqual((yield uut.rtn), 0)
            self.assertEqual((yield uut.jmp), 0)

            yield uut.i.eq(Opcodes.NOPF)
            yield en.eq(1)
            yield

            yield uut.i.eq(Opcodes.NOPO)
            yield

            self.assertEqual((yield uut.flag_f), 1)
            self.assertEqual((yield uut.flag_o), 0)
            self.assertEqual((yield uut.rtn), 0)
            self.assertEqual((yield uut.jmp), 0)

            yield uut.i.eq(Opcodes.RTN)
            yield

            self.assertEqual((yield uut.flag_f), 0)
            self.assertEqual((yield uut.flag_o), 1)
            self.assertEqual((yield uut.rtn), 0)
            self.assertEqual((yield uut.jmp), 0)

            yield uut.i.eq(Opcodes.JMP)
            yield

            self.assertEqual((yield uut.flag_f), 0)
            self.assertEqual((yield uut.flag_o), 0)
            self.assertEqual((yield uut.rtn), 1)
            self.assertEqual((yield uut.jmp), 0)

            yield uut.i.eq(Opcodes.IEN)
            yield

            self.assertEqual((yield uut.flag_f), 0)
            self.assertEqual((yield uut.flag_o), 0)
            self.assertEqual((yield uut.rtn), 0)
            self.assertEqual((yield uut.jmp), 1)

            yield

            self.assertEqual((yield uut.flag_f), 0)
            self.assertEqual((yield uut.flag_o), 0)
            self.assertEqual((yield uut.rtn), 0)
            self.assertEqual((yield uut.jmp), 0)

        self.do_sim(uut, proc, vcd_file='test.vcd')

    def test_formal(self):
        self.assertFormal(MC14500(), mode='bmc', depth=10)

if __name__ == '__main__':
    from nmigen.back import rtlil

    uut = MC14500()
    with open('mc14500.il', 'w') as f:
        f.write(rtlil.convert(uut, ports=[
            uut.write, uut.data_i, uut.data_o,
            uut.i,
            uut.flag_f, uut.flag_o, uut.rtn, uut.jmp,
            uut.rr
        ]))