Skip to content

Instantly share code, notes, and snippets.

@the6p4c
Created Nov 10, 2020
Embed
What would you like to do?
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
]))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment