Skip to content

Instantly share code, notes, and snippets.

@the6p4c

the6p4c/mc14500.py

Created November 10, 2020 11:47
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save the6p4c/3e935783e51f621d9a21d1eb00eab030 to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save the6p4c/3e935783e51f621d9a21d1eb00eab030 to your computer and use it in GitHub Desktop.
Download ZIP

Revisions

  1. the6p4c created this gist Nov 10, 2020.
    226 changes: 226 additions & 0 deletions mc14500.py
    View file
    Original file line number Diff line number Diff line change
    @@ -0,0 +1,226 @@
    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
    ]))