From f670adaed55a4bc9cf6e02aa68328a96ca5f2de8 Mon Sep 17 00:00:00 2001 From: Robert Baruch Date: Sun, 5 Jan 2020 13:53:46 -0800 Subject: [PATCH] Adds branch and flag instructions --- Makefile | 7 +-- README.md | 3 +- alu8.py | 40 ++++++++++++ core.py | 124 +++++++++++++++++++++++++++++++++++-- formal/formal_br.py | 94 ++++++++++++++++++++++++++++ formal/formal_flag.py | 70 +++++++++++++++++++++ formal/formal_inc_dec_x.py | 47 ++++++++++++++ formal/formal_tap.py | 39 ++++++++++++ formal/formal_tpa.py | 39 ++++++++++++ 9 files changed, 453 insertions(+), 10 deletions(-) create mode 100644 formal/formal_br.py create mode 100644 formal/formal_flag.py create mode 100644 formal/formal_inc_dec_x.py create mode 100644 formal/formal_tap.py create mode 100644 formal/formal_tpa.py diff --git a/Makefile b/Makefile index 30d3287..56cb024 100644 --- a/Makefile +++ b/Makefile @@ -35,17 +35,16 @@ formal_targets := $(patsubst formal/%.py, %, $(wildcard formal/formal_*.py)) formal: $(formal_targets) -formal_%: formal/sby/%_bmc/status +formal_%: formal/sby/%_bmc/PASS $(info $(shell date '+%d %b %Y %H:%M:%S') Verified instruction '$*') # Don't delete the status file if the user hits ctrl-C. -.PRECIOUS: formal/sby/%_bmc/status +# .PRECIOUS: formal/sby/%_bmc/status -formal/sby/%_bmc/status: formal/sby/%.sby +formal/sby/%_bmc/PASS: formal/sby/%.sby $(info $(shell date '+%d %b %Y %H:%M:%S') Running formal verification on instruction '$*'...) sby -f $< 2>&1 >/dev/null; if [ $$? -ne 0 ]; then \ echo `date '+%d %b %Y %H:%M:%S'` Formal verification FAILED for instruction \'$*\'; \ - rm $@; \ fi formal/sby/%.sby: formal/sby/%.il formal/formal.sby diff --git a/README.md b/README.md index 004bc7c..c969a29 100644 --- a/README.md +++ b/README.md @@ -7,4 +7,5 @@ This is a **WORK IN PROGRESS**! * Release for [video 3](https://youtu.be/aLQqOxnVMOQ): [tag 0.03.0](https://github.com/RobertBaruch/n6800/tree/0.03.0) * Release for [video 4](https://youtu.be/xqMtyCu4lME): [tag 0.04.0](https://github.com/RobertBaruch/n6800/tree/0.04.0) * Release for [video 5](https://youtu.be/9MMb9dSnNvo): [tag 0.05.1](https://github.com/RobertBaruch/n6800/tree/0.05.1) -* Release for [video 6](https://youtu.be/C6sUaElP9hA): [tag 0.06.0](https://github.com/RobertBaruch/n6800/tree/0.06.0) \ No newline at end of file +* Release for [video 6](https://youtu.be/C6sUaElP9hA): [tag 0.06.0](https://github.com/RobertBaruch/n6800/tree/0.06.0) +* Release for [video 7](https://youtu.be/AerXEa84jsc): [tag 0.07.0](https://github.com/RobertBaruch/n6800/tree/0.07.0) \ No newline at end of file diff --git a/alu8.py b/alu8.py index 3f7eb10..12b61fa 100644 --- a/alu8.py +++ b/alu8.py @@ -38,6 +38,16 @@ class ALU8Func(IntEnum): # CMP is the same as SUB, just don't store the output. EOR = 7 ORA = 8 + CLV = 9 + SEV = 10 + CLC = 11 + SEC = 12 + TAP = 13 + TPA = 14 + CLI = 15 + SEI = 16 + CLZ = 17 + SEZ = 18 class ALU8(Elaboratable): @@ -122,6 +132,36 @@ def elaborate(self, platform: Platform) -> Module: m.d.comb += self._ccs[Flags.N].eq(self.output[7]) m.d.comb += self._ccs[Flags.V].eq(0) + with m.Case(ALU8Func.CLC): + m.d.comb += self._ccs[Flags.C].eq(0) + + with m.Case(ALU8Func.SEC): + m.d.comb += self._ccs[Flags.C].eq(1) + + with m.Case(ALU8Func.CLV): + m.d.comb += self._ccs[Flags.V].eq(0) + + with m.Case(ALU8Func.SEV): + m.d.comb += self._ccs[Flags.V].eq(1) + + with m.Case(ALU8Func.CLI): + m.d.comb += self._ccs[Flags.I].eq(0) + + with m.Case(ALU8Func.SEI): + m.d.comb += self._ccs[Flags.I].eq(1) + + with m.Case(ALU8Func.CLZ): + m.d.comb += self._ccs[Flags.Z].eq(0) + + with m.Case(ALU8Func.SEZ): + m.d.comb += self._ccs[Flags.Z].eq(1) + + with m.Case(ALU8Func.TAP): + m.d.comb += self._ccs.eq(self.input1 | 0b11000000) + + with m.Case(ALU8Func.TPA): + m.d.comb += self.output.eq(self.ccs | 0b11000000) + return m diff --git a/core.py b/core.py index 62f2d79..c729b03 100644 --- a/core.py +++ b/core.py @@ -28,9 +28,9 @@ from formal.verification import FormalData, Verification from alu8 import ALU8Func, ALU8 -from consts.consts import ModeBits +from consts.consts import ModeBits, Flags -from nmigen import Signal, Value, Elaboratable, Module, Cat, Const, Mux +from nmigen import Signal, Value, Elaboratable, Module, Cat, Const, Mux, signed from nmigen import ClockDomain, ClockSignal from nmigen.hdl.ast import Statement from nmigen.asserts import Assert, Past, Cover, Assume @@ -260,6 +260,20 @@ def execute(self, m: Module): with m.Switch(self.instr): with m.Case("00000001"): # NOP self.NOP(m) + with m.Case("00000110"): # TAP + self.TAP(m) + with m.Case("00000111"): # TPA + self.TPA(m) + with m.Case("0000100-"): # INX/DEX + self.IN_DE_X(m) + with m.Case("0000101-"): # CLV, SEV + self.CL_SE_V(m) + with m.Case("0000110-"): # CLC, SEC + self.CL_SE_C(m) + with m.Case("0000111-"): # CLI, SEI + self.CL_SE_I(m) + with m.Case("0010----"): # Branch instructions + self.BR(m) with m.Case("011-1110"): # JMP self.JMP(m) with m.Case("1---0110"): # LDA @@ -360,6 +374,60 @@ def ALU(self, m: Module, func: ALU8Func, store: bool = True): m.d.ph1 += self.a.eq(self.alu8) self.end_instr(m, self.pc) + def BR(self, m: Module): + operand = self.mode_immediate8(m) + + relative = Signal(signed(8)) + m.d.comb += relative.eq(operand) + + # At this point, pc is the instruction start + 2, so we just + # add the signed relative offset to get the target. + with m.If(self.cycle == 2): + m.d.ph1 += self.tmp16.eq(self.pc + relative) + + with m.If(self.cycle == 3): + take_branch = self.branch_check(m) + self.end_instr(m, Mux(take_branch, self.tmp16, self.pc)) + + def CL_SE_C(self, m: Module): + """Clears or sets Carry.""" + with m.If(self.cycle == 1): + m.d.comb += self.alu8_func.eq( + Mux(self.instr[0], ALU8Func.SEC, ALU8Func.CLC)) + self.end_instr(m, self.pc) + + def CL_SE_V(self, m: Module): + """Clears or sets Overflow.""" + with m.If(self.cycle == 1): + m.d.comb += self.alu8_func.eq( + Mux(self.instr[0], ALU8Func.SEV, ALU8Func.CLV)) + self.end_instr(m, self.pc) + + def CL_SE_I(self, m: Module): + """Clears or sets Interrupt.""" + with m.If(self.cycle == 1): + m.d.comb += self.alu8_func.eq( + Mux(self.instr[0], ALU8Func.SEI, ALU8Func.CLI)) + self.end_instr(m, self.pc) + + def IN_DE_X(self, m: Module): + """Increments or decrements X.""" + dec = self.instr[0] + + with m.If(self.cycle == 1): + m.d.ph1 += self.VMA.eq(0) + m.d.ph1 += self.Addr.eq(self.x) + m.d.ph1 += self.x.eq(Mux(dec, self.x - 1, self.x + 1)) + + with m.If(self.cycle == 2): + m.d.ph1 += self.VMA.eq(0) + m.d.ph1 += self.Addr.eq(self.x) + + with m.If(self.cycle == 3): + m.d.comb += self.alu8_func.eq( + Mux(self.x == 0, ALU8Func.SEZ, ALU8Func.CLZ)) + self.end_instr(m, self.pc) + def JMP(self, m: Module): with m.If(self.mode == ModeBits.EXTENDED.value): operand = self.mode_ext(m) @@ -439,6 +507,52 @@ def STA(self, m: Module): m.d.comb += self.alu8_func.eq(ALU8Func.LD) self.end_instr(m, self.pc) + def TAP(self, m: Module): + """Transfer A to CCS.""" + with m.If(self.cycle == 1): + m.d.comb += self.alu8_func.eq(ALU8Func.TAP) + m.d.comb += self.src8_1.eq(self.a) + self.end_instr(m, self.pc) + + def TPA(self, m: Module): + """Transfer CCS to A.""" + with m.If(self.cycle == 1): + m.d.comb += self.alu8_func.eq(ALU8Func.TPA) + m.d.ph1 += self.a.eq(self.alu8) + self.end_instr(m, self.pc) + + def branch_check(self, m: Module) -> Signal: + """Generates logic for a 1-bit value for branching. + + Returns a 1-bit Signal which is set if the branch should be + taken. The branch logic is determined by the instruction. + """ + invert = self.instr[0] + cond = Signal() + take_branch = Signal() + + with m.Switch(self.instr[1:4]): + with m.Case("000"): # BRA, BRN + m.d.comb += cond.eq(1) + with m.Case("001"): # BHI, BLS + m.d.comb += cond.eq(~(self.ccs[Flags.C] | self.ccs[Flags.Z])) + with m.Case("010"): # BCC, BCS + m.d.comb += cond.eq(~self.ccs[Flags.C]) + with m.Case("011"): # BNE, BEQ + m.d.comb += cond.eq(~self.ccs[Flags.Z]) + with m.Case("100"): # BVC, BVS + m.d.comb += cond.eq(~self.ccs[Flags.V]) + with m.Case("101"): # BPL, BMI + m.d.comb += cond.eq(~self.ccs[Flags.N]) + with m.Case("110"): # BGE, BLT + m.d.comb += cond.eq(~(self.ccs[Flags.N] ^ self.ccs[Flags.V])) + with m.Case("111"): # BGT, BLE + m.d.comb += cond.eq(~(self.ccs[Flags.Z] | + (self.ccs[Flags.N] ^ self.ccs[Flags.V]))) + + m.d.comb += take_branch.eq(cond ^ invert) + return take_branch + def mode_immediate8(self, m: Module) -> Statement: """Generates logic to get the 8-bit operand for immediate mode instructions. @@ -582,9 +696,9 @@ def end_instr(self, m: Module, addr: Statement): mem = { 0xFFFE: 0x12, 0xFFFF: 0x34, - 0x1234: 0x7E, # JMP 0xA010 - 0x1235: 0xA0, - 0x1236: 0x10, + 0x1234: 0x20, # BRA 0x1234 + 0x1235: 0xFE, + 0x1236: 0x01, # NOP 0xA010: 0x01, # NOP } with m.Switch(core.Addr): diff --git a/formal/formal_br.py b/formal/formal_br.py new file mode 100644 index 0000000..0e82655 --- /dev/null +++ b/formal/formal_br.py @@ -0,0 +1,94 @@ +# Copyright (C) 2020 Robert Baruch +# +# This program is free software: you can redistribute it and/or modify +# it under the terms of the GNU General Public License as published by +# the Free Software Foundation, either version 3 of the License, or +# (at your option) any later version. +# +# This program is distributed in the hope that it will be useful, +# but WITHOUT ANY WARRANTY; without even the implied warranty of +# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +# GNU General Public License for more details. +# +# You should have received a copy of the GNU General Public License +# along with this program. If not, see . + +from enum import IntEnum + +from nmigen import Signal, Value, Cat, Module, signed, Mux, Const, Array +from nmigen.hdl.ast import Statement +from nmigen.asserts import Assert +from .verification import FormalData, Verification +from consts.consts import Flags + + +class Branch(IntEnum): + """Encodings for the low 4 bits of branch instructions.""" + A = 0x0 + N = 0x1 + HI = 0x2 + LS = 0x3 + CC = 0x4 + CS = 0x5 + NE = 0x6 + EQ = 0x7 + VC = 0x8 + VS = 0x9 + PL = 0xA + MI = 0xB + GE = 0xC + LT = 0xD + GT = 0xE + LE = 0xF + + +class Formal(Verification): + def __init__(self): + pass + + def valid(self, instr: Value) -> Value: + return instr.matches("0010----") + + def check(self, m: Module, instr: Value, data: FormalData): + m.d.comb += [ + Assert(data.post_ccs == data.pre_ccs), + Assert(data.post_a == data.pre_a), + Assert(data.post_b == data.pre_b), + Assert(data.post_x == data.pre_x), + Assert(data.post_sp == data.pre_sp), + Assert(data.addresses_written == 0), + ] + + m.d.comb += [ + Assert(data.addresses_read == 1), + Assert(data.read_addr[0] == data.plus16(data.pre_pc, 1)), + ] + + n = data.pre_ccs[Flags.N] + z = data.pre_ccs[Flags.Z] + v = data.pre_ccs[Flags.V] + c = data.pre_ccs[Flags.C] + offset = Signal(signed(8)) + br = instr[:4] + + take_branch = Array([ + Const(1), + Const(0), + (c | z) == 0, + (c | z) == 1, + c == 0, + c == 1, + z == 0, + z == 1, + v == 0, + v == 1, + n == 0, + n == 1, + (n ^ v) == 0, + (n ^ v) == 1, + (z | (n ^ v)) == 0, + (z | (n ^ v)) == 1, + ]) + m.d.comb += offset.eq(data.read_data[0]) + m.d.comb += Assert(data.post_pc == Mux( + take_branch[br], (data.pre_pc + 2 + offset)[:16], (data.pre_pc + 2)[:16])) diff --git a/formal/formal_flag.py b/formal/formal_flag.py new file mode 100644 index 0000000..275d431 --- /dev/null +++ b/formal/formal_flag.py @@ -0,0 +1,70 @@ +# Copyright (C) 2020 Robert Baruch +# +# This program is free software: you can redistribute it and/or modify +# it under the terms of the GNU General Public License as published by +# the Free Software Foundation, either version 3 of the License, or +# (at your option) any later version. +# +# This program is distributed in the hope that it will be useful, +# but WITHOUT ANY WARRANTY; without even the implied warranty of +# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +# GNU General Public License for more details. +# +# You should have received a copy of the GNU General Public License +# along with this program. If not, see . + +from nmigen import Signal, Value, Cat, Module, Mux +from nmigen.hdl.ast import Statement +from nmigen.asserts import Assert +from .verification import FormalData, Verification +from consts.consts import Flags + +CLV = "00001010" +SEV = "00001011" +CLC = "00001100" +SEC = "00001101" +CLI = "00001110" +SEI = "00001111" + + +class Formal(Verification): + def __init__(self): + pass + + def valid(self, instr: Value) -> Value: + return instr.matches(CLV, SEV, CLC, SEC, CLI, SEI) + + def check(self, m: Module, instr: Value, data: FormalData): + m.d.comb += [ + Assert(data.post_a == data.pre_a), + Assert(data.post_b == data.pre_b), + Assert(data.post_x == data.pre_x), + Assert(data.post_sp == data.pre_sp), + Assert(data.addresses_written == 0), + Assert(data.addresses_read == 0), + ] + m.d.comb += Assert(data.post_pc == data.plus16(data.pre_pc, 1)) + + c = Signal() + v = Signal() + i = Signal() + + m.d.comb += c.eq(data.pre_ccs[Flags.C]) + m.d.comb += v.eq(data.pre_ccs[Flags.V]) + m.d.comb += i.eq(data.pre_ccs[Flags.I]) + + with m.Switch(instr): + with m.Case(CLV): + m.d.comb += v.eq(0) + with m.Case(SEV): + m.d.comb += v.eq(1) + with m.Case(CLC): + m.d.comb += c.eq(0) + with m.Case(SEC): + m.d.comb += c.eq(1) + with m.Case(CLI): + m.d.comb += i.eq(0) + with m.Case(SEI): + m.d.comb += i.eq(1) + + self.assertFlags(m, data.post_ccs, data.pre_ccs, V=v, C=c, I=i) diff --git a/formal/formal_inc_dec_x.py b/formal/formal_inc_dec_x.py new file mode 100644 index 0000000..59772a1 --- /dev/null +++ b/formal/formal_inc_dec_x.py @@ -0,0 +1,47 @@ +# Copyright (C) 2020 Robert Baruch +# +# This program is free software: you can redistribute it and/or modify +# it under the terms of the GNU General Public License as published by +# the Free Software Foundation, either version 3 of the License, or +# (at your option) any later version. +# +# This program is distributed in the hope that it will be useful, +# but WITHOUT ANY WARRANTY; without even the implied warranty of +# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +# GNU General Public License for more details. +# +# You should have received a copy of the GNU General Public License +# along with this program. If not, see . + +from nmigen import Signal, Value, Cat, Module, Mux +from nmigen.hdl.ast import Statement +from nmigen.asserts import Assert +from .verification import FormalData, Verification + +INX = "00001000" +DEX = "00001001" + + +class Formal(Verification): + def __init__(self): + pass + + def valid(self, instr: Value) -> Value: + return instr.matches(INX, DEX) + + def check(self, m: Module, instr: Value, data: FormalData): + m.d.comb += [ + Assert(data.post_a == data.pre_a), + Assert(data.post_b == data.pre_b), + Assert(data.post_sp == data.pre_sp), + Assert(data.addresses_written == 0), + Assert(data.addresses_read == 0), + ] + m.d.comb += Assert(data.post_pc == data.plus16(data.pre_pc, 1)) + + with m.If(instr.matches(INX)): + m.d.comb += Assert(data.post_x == (data.pre_x + 1)[:16]) + with m.If(instr.matches(DEX)): + m.d.comb += Assert(data.post_x == (data.pre_x - 1)[:16]) + + self.assertFlags(m, data.post_ccs, data.pre_ccs, Z=(data.post_x == 0)) diff --git a/formal/formal_tap.py b/formal/formal_tap.py new file mode 100644 index 0000000..3f0b77b --- /dev/null +++ b/formal/formal_tap.py @@ -0,0 +1,39 @@ +# Copyright (C) 2020 Robert Baruch +# +# This program is free software: you can redistribute it and/or modify +# it under the terms of the GNU General Public License as published by +# the Free Software Foundation, either version 3 of the License, or +# (at your option) any later version. +# +# This program is distributed in the hope that it will be useful, +# but WITHOUT ANY WARRANTY; without even the implied warranty of +# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +# GNU General Public License for more details. +# +# You should have received a copy of the GNU General Public License +# along with this program. If not, see . + +from nmigen import Signal, Value, Cat, Module, Mux +from nmigen.hdl.ast import Statement +from nmigen.asserts import Assert +from .verification import FormalData, Verification + + +class Formal(Verification): + def __init__(self): + pass + + def valid(self, instr: Value) -> Value: + return instr.matches("00000110") + + def check(self, m: Module, instr: Value, data: FormalData): + m.d.comb += [ + Assert(data.post_a == data.pre_a), + Assert(data.post_b == data.pre_b), + Assert(data.post_x == data.pre_x), + Assert(data.post_sp == data.pre_sp), + Assert(data.addresses_written == 0), + Assert(data.addresses_read == 0), + ] + m.d.comb += Assert(data.post_pc == data.plus16(data.pre_pc, 1)) + m.d.comb += Assert(data.post_ccs == (0b11000000 | data.pre_a)) diff --git a/formal/formal_tpa.py b/formal/formal_tpa.py new file mode 100644 index 0000000..76345c3 --- /dev/null +++ b/formal/formal_tpa.py @@ -0,0 +1,39 @@ +# Copyright (C) 2020 Robert Baruch +# +# This program is free software: you can redistribute it and/or modify +# it under the terms of the GNU General Public License as published by +# the Free Software Foundation, either version 3 of the License, or +# (at your option) any later version. +# +# This program is distributed in the hope that it will be useful, +# but WITHOUT ANY WARRANTY; without even the implied warranty of +# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +# GNU General Public License for more details. +# +# You should have received a copy of the GNU General Public License +# along with this program. If not, see . + +from nmigen import Signal, Value, Cat, Module, Mux +from nmigen.hdl.ast import Statement +from nmigen.asserts import Assert +from .verification import FormalData, Verification + + +class Formal(Verification): + def __init__(self): + pass + + def valid(self, instr: Value) -> Value: + return instr.matches("00000111") + + def check(self, m: Module, instr: Value, data: FormalData): + m.d.comb += [ + Assert(data.post_ccs == data.pre_ccs), + Assert(data.post_b == data.pre_b), + Assert(data.post_x == data.pre_x), + Assert(data.post_sp == data.pre_sp), + Assert(data.addresses_written == 0), + Assert(data.addresses_read == 0), + ] + m.d.comb += Assert(data.post_pc == data.plus16(data.pre_pc, 1)) + m.d.comb += Assert(data.post_a == (0b11000000 | data.pre_ccs))