I am having a problem running the CPU with the rom for the APF M1000

The problem is that I am getting intermittent stack corruption. The symptom is that a return address on the stack gets duplicated and sp is then permanently decremented by 2. After this happens a few times, the stack overflows.

Looking at what happens when an interrupt is taken at the end of of a RTS instruction, on the last cycle of the RTS, sp is set to Addr (see https://github.com/RobertBaruch/n6800/blob/master/core.py#L913). Then in end_instr_flag_handler, on the same cycle, Addr is set to sp (see https://github.com/RobertBaruch/n6800/blob/master/core.py#L213). I am not sure if this is valid.

As a temporary fix, I tried changing RTS to use an extra cycle, so that setting sp, and ending the instruction are on separate cycles. This appears to fix the problem.

See https://github.com/RobertBaruch/n6800/blob/master/core.py#L372

The line should be:

with m.Case("0001011-"):  # TAB, TBA

I found that while trying to implement a 6800 retro computer (the APF M1000, or Imagination Machine) on a Ulx3s board, see https://github.com/lawrie/ulx3s-nmigen-examples/tree/master/retro

Found a bug, which might be nasty once cycle count for instruction will be around 9 that formal verification doesn't cover a case of single instruction that went into endless loop

To demonstrate: in mode_ext,

 with m.If(self.cycle == 1): 
        ....
        m.d.ph1 += self.cycle.eq(2)

replace 2 with 1 so whole branch looks like this

   with m.If(self.cycle == 1):
        m.d.ph1 += self.tmp16[8:].eq(self.Din)
        m.d.ph1 += self.pc.eq(self.pc + 1)
        m.d.ph1 += self.Addr.eq(self.pc + 1)
        m.d.ph1 += self.RW.eq(1)
        m.d.ph1 += self.cycle.eq(1) ### Introduced error
        if self.verification is not None:
            self.formalData.read(m, self.Addr, self.Din)

if you run simulation and look at traces, JMP 0xA010 will not be executed: PC will be increasing by 1 each cycle.
However running tests over python3 core.py --insn jmp generate -t il core.il will pass both cover and bmc.

This happens because we don't check if instruction was actually finished, only that it was started:

• we cover that core.formalData.snapshot_taken, it was the at start of the instruction
• the meat of the verification, self.verification.check only gets called on the start of next instruction (cycle=0).