Adds branch and flag instructions

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

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)
+* 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)

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
 
 

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):

formal/formal_br.py

@@ -0,0 +1,94 @@
+# Copyright (C) 2020 Robert Baruch <[email protected]>
+#
+# 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 <https://www.gnu.org/licenses/>.
+
+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]))