Adds all insns except RTI, WAI, SWI.

.gitignore

@@ -135,3 +135,5 @@ dmypy.json
 
 # Pyre type checker
 .pyre/
+
+.vscode/settings.json

Makefile

@@ -53,3 +53,6 @@ formal/sby/%.sby: formal/sby/%.il formal/formal.sby
 
 formal/sby/%.il: formal/formal_%.py core.py
 	python3 core.py --insn $* generate -t il > $@
+
+formal/sby/alu8.il: alu8.py
+	python3 alu8.py generate -t il > $@

README.md

@@ -9,4 +9,5 @@ This is a **WORK IN PROGRESS**!
 * 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 7](https://youtu.be/AerXEa84jsc): [tag 0.07.0](https://github.com/RobertBaruch/n6800/tree/0.07.0)
-* Release for [video 8](https://youtu.be/6acCiGBjM6s): [tag 0.08.0](https://github.com/RobertBaruch/n6800/tree/0.08.0)
+* Release for [video 8](https://youtu.be/6acCiGBjM6s): [tag 0.08.0](https://github.com/RobertBaruch/n6800/tree/0.08.0)
+* Release for [video 9](https://youtu.be/Xe1cbCZIaKQ): [tag 0.09.0](https://github.com/RobertBaruch/n6800/tree/0.09.0)

alu8.py

@@ -23,7 +23,7 @@
 from nmigen import ClockDomain, ClockSignal
 from nmigen.build import Platform
 from nmigen.cli import main_parser, main_runner
-from nmigen.asserts import Assert, Assume
+from nmigen.asserts import Assert, Assume, Cover, Past
 
 
 class ALU8Func(IntEnum):
@@ -56,6 +56,18 @@ class ALU8Func(IntEnum):
     ASL = 24
     ASR = 25
     LSR = 26
+    DAA = 27
+    # LDCHAIN assumes the high byte of a 16-bit value has already
+    # been passed through LD, so N and Z have been evaluated. LDCHAIN
+    # is then used on the low byte, so N should not be changed, and
+    # Z should be anded with low_byte == 0.
+    LDCHAIN = 28
+    # CPXHI is the same as SUB, but doesn't set the C flag.
+    CPXHI = 29
+    # CPXLO assumes the high byte of a 16-bit value has already
+    # been passed through CPXHI, so N, V, and Z have been evaluated.
+    # Z should be anded with whether the subtraction is zero.
+    CPXLO = 30
 
 
 def LCat(*args) -> Value:
@@ -99,6 +111,12 @@ 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.LDCHAIN):
+                m.d.comb += self.output.eq(self.input2)
+                m.d.comb += self._ccs[Flags.Z].eq(
+                    (self.output == 0) & self.ccs[Flags.Z])
+                m.d.comb += self._ccs[Flags.V].eq(0)
+
             with m.Case(ALU8Func.ADD, ALU8Func.ADC):
                 carry_in = Mux(self.func == ALU8Func.ADD, 0, self.ccs[Flags.C])
 
@@ -117,19 +135,25 @@ def elaborate(self, platform: Platform) -> Module:
                 m.d.comb += self._ccs[Flags.V].eq(overflow)
                 m.d.comb += self._ccs[Flags.C].eq(carry8)
 
-            with m.Case(ALU8Func.SUB, ALU8Func.SBC):
-                carry_in = Mux(self.func == ALU8Func.SUB, 0, self.ccs[Flags.C])
+            with m.Case(ALU8Func.SUB, ALU8Func.SBC, ALU8Func.CPXHI, ALU8Func.CPXLO):
+                carry_in = Mux(self.func != ALU8Func.SBC, 0, self.ccs[Flags.C])
 
                 sum0_6 = Cat(self.output[:7], carry7)
                 m.d.comb += sum0_6.eq(self.input1[:7] +
                                       ~self.input2[:7] + ~carry_in)
                 sum7 = Cat(self.output[7], carry8)
                 m.d.comb += sum7.eq(self.input1[7] + ~self.input2[7] + carry7)
                 m.d.comb += overflow.eq(carry7 ^ carry8)
-                m.d.comb += self._ccs[Flags.N].eq(self.output[7])
-                m.d.comb += self._ccs[Flags.Z].eq(self.output == 0)
-                m.d.comb += self._ccs[Flags.V].eq(overflow)
-                m.d.comb += self._ccs[Flags.C].eq(~carry8)
+
+                with m.If(self.func != ALU8Func.CPXLO):
+                    m.d.comb += self._ccs[Flags.N].eq(self.output[7])
+                    m.d.comb += self._ccs[Flags.Z].eq(self.output == 0)
+                    m.d.comb += self._ccs[Flags.V].eq(overflow)
+                    with m.If(self.func != ALU8Func.CPXHI):
+                        m.d.comb += self._ccs[Flags.C].eq(~carry8)
+                with m.Else():
+                    m.d.comb += self._ccs[Flags.Z].eq(
+                        (self.output == 0) & self.ccs[Flags.Z])
 
             with m.Case(ALU8Func.AND):
                 m.d.comb += self.output.eq(self.input1 & self.input2)
@@ -258,6 +282,24 @@ def elaborate(self, platform: Platform) -> Module:
             with m.Case(ALU8Func.TPA):
                 m.d.comb += self.output.eq(self.ccs | 0b11000000)
 
+            with m.Case(ALU8Func.DAA):
+                adjust = Signal(8)
+                low = self.input1[:4]
+                high = self.input1[4:]
+                low_ten_or_more = low >= 0xA
+                high_ten_or_more = high >= 0xA
+
+                with m.If(low_ten_or_more | self.ccs[Flags.H]):
+                    m.d.comb += adjust[:4].eq(6)
+                with m.If(high_ten_or_more | self.ccs[Flags.C] | (low_ten_or_more & (high == 9))):
+                    m.d.comb += adjust[4:].eq(6)
+                sum9 = LCat(carry8, self.output)
+
+                m.d.comb += sum9.eq(self.input1 + adjust)
+                m.d.comb += self._ccs[Flags.N].eq(self.output[7])
+                m.d.comb += self._ccs[Flags.Z].eq(self.output == 0)
+                m.d.comb += self._ccs[Flags.C].eq(carry8 | self.ccs[Flags.C])
+
         return m
 
 
@@ -273,58 +315,96 @@ def elaborate(self, platform: Platform) -> Module:
     ph1clk = ClockSignal("ph1")
     ph1.rst = rst
 
+    test_daa = Signal()
+    m.submodules.alu2 = alu2 = ALU8()
+
     carry_in = Signal()
     sum9 = Signal(9)
     sum8 = Signal(8)
     sum5 = Signal(5)
 
+    m.d.ph1 += Assume(rst == 0)
     m.d.comb += Assert(alu._ccs[6:] == 0b11)
 
-    with m.Switch(alu.func):
-        with m.Case(ALU8Func.ADD, ALU8Func.ADC):
-            # sumN = input1[:N] + input2[:N] (so sumN[N-1] is the carry bit)
-            with m.If(alu.func == ALU8Func.ADD):
-                m.d.comb += carry_in.eq(0)
-            with m.Else():
-                m.d.comb += carry_in.eq(alu.ccs[Flags.C])
-            h = sum5[4]
-            n = sum9[7]
-            c = sum9[8]
-            z = (sum9[:8] == 0)
-            v = (sum8[7] ^ c)
-            m.d.comb += [
-                sum9.eq(alu.input1 + alu.input2 + carry_in),
-                sum8.eq(alu.input1[:7] + alu.input2[:7] + carry_in),
-                sum5.eq(alu.input1[:4] + alu.input2[:4] + carry_in),
-                Assert(alu.output == sum9[:8]),
-                Assert(alu._ccs[Flags.H] == h),
-                Assert(alu._ccs[Flags.N] == n),
-                Assert(alu._ccs[Flags.Z] == z),
-                Assert(alu._ccs[Flags.V] == v),
-                Assert(alu._ccs[Flags.C] == c),
-                Assert(alu._ccs[Flags.I] == alu.ccs[Flags.I]),
-            ]
-        with m.Case(ALU8Func.SUB, ALU8Func.SBC):
-            with m.If(alu.func == ALU8Func.SUB):
-                m.d.comb += carry_in.eq(0)
-            with m.Else():
-                m.d.comb += carry_in.eq(alu.ccs[Flags.C])
-            n = sum9[7]
-            c = ~sum9[8]
-            z = (sum9[:8] == 0)
-            v = (sum8[7] ^ sum9[8])
-            m.d.comb += [
-                sum9.eq(alu.input1 + ~alu.input2 + ~carry_in),
-                sum8.eq(alu.input1[:7] + ~alu.input2[:7] + ~carry_in),
-                Assert(sum9[:8] == (
-                    alu.input1 - alu.input2 - carry_in)[:8]),
-                Assert(alu.output == sum9[:8]),
-                Assert(alu._ccs[Flags.N] == n),
-                Assert(alu._ccs[Flags.Z] == z),
-                Assert(alu._ccs[Flags.V] == v),
-                Assert(alu._ccs[Flags.C] == c),
-                Assert(alu._ccs[Flags.H] == alu.ccs[Flags.H]),
-                Assert(alu._ccs[Flags.I] == alu.ccs[Flags.I]),
-            ]
-
-    main_runner(parser, args, m, ports=alu.input_ports() + [ph1clk, rst])
+    with m.If((~test_daa) | ~Past(test_daa)):
+        with m.Switch(alu.func):
+            with m.Case(ALU8Func.ADD, ALU8Func.ADC):
+                # sumN = input1[:N] + input2[:N] (so sumN[N-1] is the carry bit)
+                with m.If(alu.func == ALU8Func.ADD):
+                    m.d.comb += carry_in.eq(0)
+                with m.Else():
+                    m.d.comb += carry_in.eq(alu.ccs[Flags.C])
+                h = sum5[4]
+                n = sum9[7]
+                c = sum9[8]
+                z = (sum9[:8] == 0)
+                v = (sum8[7] ^ c)
+                m.d.comb += [
+                    sum9.eq(alu.input1 + alu.input2 + carry_in),
+                    sum8.eq(alu.input1[:7] + alu.input2[:7] + carry_in),
+                    sum5.eq(alu.input1[:4] + alu.input2[:4] + carry_in),
+                    Assert(alu.output == sum9[:8]),
+                    Assert(alu._ccs[Flags.H] == h),
+                    Assert(alu._ccs[Flags.N] == n),
+                    Assert(alu._ccs[Flags.Z] == z),
+                    Assert(alu._ccs[Flags.V] == v),
+                    Assert(alu._ccs[Flags.C] == c),
+                    Assert(alu._ccs[Flags.I] == alu.ccs[Flags.I]),
+                ]
+            with m.Case(ALU8Func.SUB, ALU8Func.SBC):
+                with m.If(alu.func == ALU8Func.SUB):
+                    m.d.comb += carry_in.eq(0)
+                with m.Else():
+                    m.d.comb += carry_in.eq(alu.ccs[Flags.C])
+                n = sum9[7]
+                c = ~sum9[8]
+                z = (sum9[:8] == 0)
+                v = (sum8[7] ^ sum9[8])
+                m.d.comb += [
+                    sum9.eq(alu.input1 + ~alu.input2 + ~carry_in),
+                    sum8.eq(alu.input1[:7] + ~alu.input2[:7] + ~carry_in),
+                    Assert(sum9[:8] == (
+                        alu.input1 - alu.input2 - carry_in)[:8]),
+                    Assert(alu.output == sum9[:8]),
+                    Assert(alu._ccs[Flags.N] == n),
+                    Assert(alu._ccs[Flags.Z] == z),
+                    Assert(alu._ccs[Flags.V] == v),
+                    Assert(alu._ccs[Flags.C] == c),
+                    Assert(alu._ccs[Flags.H] == alu.ccs[Flags.H]),
+                    Assert(alu._ccs[Flags.I] == alu.ccs[Flags.I]),
+                ]
+
+    with m.Else():  # test_daa
+        in1_lo = Past(alu.input1)[:4]
+        in1_hi = Past(alu.input1)[4:]
+        in2_lo = Past(alu.input2)[:4]
+        in2_hi = Past(alu.input2)[4:]
+        in_carry = Past(alu.ccs)[Flags.C]
+        out_lo = alu.output[:4]
+        out_hi = alu.output[4:]
+        out_carry = alu._ccs[Flags.C]
+
+        in1_dec = 10 * in1_hi + in1_lo
+        in2_dec = 10 * in2_hi + in2_lo
+        out_dec = 100 * out_carry + 10 * out_hi + out_lo
+
+        m.d.ph1 += [
+            Assume(Past(alu.func) == ALU8Func.ADC),
+            Assume(alu.func == ALU8Func.DAA),
+            Assume(alu.input1 == Past(alu.output)),
+            Assume(in1_lo < 10),
+            Assume(in1_hi < 10),
+            Assume(in2_lo < 10),
+            Assume(in2_hi < 10),
+        ]
+
+        m.d.ph1 += [
+            Assert((in1_dec + in2_dec + in_carry) == out_dec),
+            Assert(alu._ccs[Flags.N] == alu.output[7]),
+            Assert(alu._ccs[Flags.Z] == (alu.output == 0)),
+        ]
+
+        m.d.ph1 += Cover(out_dec == 142)
+
+    main_runner(parser, args, m, ports=alu.input_ports() +
+                alu2.input_ports() + [ph1clk, rst, test_daa])