Hello everyone,

I have been trying to formally verify the correctness of the opencores 8051 implementation. While doing this, I seem to have run into something that could be a bug or could also be a misunderstanding of the spec on my part.

I have a program which executes the AJMP instruction at PC=16'hFFFC. In other words, I have PC=16'hFFFC; opcode at PC=8'h01 and the opcode at PC+1 = 8'h03.

According to my understanding of the AJMP instruction. We must calculate the next PC as follows.

1. We compute the address of the instruction following AJMP. This is PC+2 = 16'hFFFC + 2 = 16'hFFFE.
2. Next we take the upper 5 bits of this instruction (5'b 1111 1) and use this as the upper 5 bits (15-11) of the next PC.
3. Next we take the upper 3 bits of the first byte of the opcode (3'b000) and these are bits 10-8 of the next PC.
4. Finally the lower 8 bits of the next PC is equal to the second byte of the opcode, which is 03.
5. So the next PC must be (16'b 1111 1000 0000 0003) = 16'hF803.

However, oc8051 seems to compute the next PC as 16'h0003.

Is my above computation of the next PC correct? If not, can someone please let me know what I'm doing wrong? If my computation is correct, am I right in saying that there is a bug in the oc8051 or am I missing something here?

Any feedback on the above will be very helpful.

Thank you,
Pramod

You are interpreting the AJMP instruction correctly. I would guess that you would see a similar bug if you placed an AJMP at address 16'h00FC as well.

I did a cursory look at the rtl shows that the upper bits are not latched when the bits in the opcode are latched, so the pipelining in memory_interface.v may cause it to grab the upper bits after they have rolled over.

Thanks tblackmon!

I fixed this by adding the following lines to oc8051_memory_interface.

First I have:
wire [15:0] pc_plus_2 = pc + 2;

And in the case statement that writes to pc_buf, I changed the I11 line to be:
`OC8051_PIS_I11: pc_buf <= #1 {pc_plus_2[15:11], op1_out[7:5], op2_out};

I haven't yet succeeded in get an unbounded (i.e., complete) proof from the model checker that this is right, but it couldn't find any short counterexamples, so there is some reason to believe this is correct.