% ISPS Description of the MOS Technology MCS 6502 Microprocessor

%	G.W.Leive
%	10 July 1978		ISPS Version
%	COPYRIGHT (C) 1978

%	rewriten for Tokio

% MC6502 :-

'$function'  bit(Bit,I) = ( I >> Bit ) /\ 1 :-true .
'$function'  high(Word) = (Word>>8)/\hex("ff") :-true .
'$function'  low(Word)  = (Word/\hex("ff")) :-true .
'$function'  signed(Data)  = Signed :- signed(Data,Signed) .
'$function'  byte(Word)  = (Word/\hex("ff")) :-true .

signed(Data,Signed) :- Data >127,!, Signed = Data - 256.
signed(Data,Data).

:-op(600,xfy, xor).
'$function'  xor(A,B)   = ( (-A) /\ B) \/ (A /\ (-B)) :-true .

:-static([
	mem(_),

% *PCSTATE

	pc,		% program counter
	y,		% Index register
	x,		% Index register
	s,		% stack pointer
	dl,		% Input data latch
	a,		% accumulator
	ir,		% Instruction register
	p,		% processor status

	n,		% Negative result
	v,		% Overflow
	b,		% Break command
	d,		% Decimal mode
	i,		% Interrupt disable
	z,		% Zero
	c,		% Carry

	irq,		% Interrupt request
	nmi,		% Non-maskable interrupt
	ifsync,		% High when instruction fetch
	rw,		% Read/Write control pin
	so,		% set overflow pin
	reset,		% power up bit
	ready		% 1 means run, 0 means stop

]).

status_report :-
	write(('pc=',*pc,' y=', *y, ' x=',*x , ' dl=', *dl,
		' a=',*a,' ir=',*ir, ' rw=', *rw, 
		' s=',*s, ' c=', *c, ' z=' ,*z)).


% ADDRESS.CALCULATION

immed(R):- 		% Immediate
	R <- *pc,
	*pc <= *pc + 1.

zp(R):- 		% Zero page
	read(*pc,R) , *pc <= *pc + 1.

abs(R):- 		% Absolute
	ab(*pc + 1, *pc,R),
	*pc <= *pc + 2.

indx(R):- 		% Indexed indirect - (IND, *x)
	read(*pc,R) &&
	R1 = R + *x, read_2(R1+1,R1,H,L) &&
	ab(H,L,R), *pc <= *pc + 1.

indy(R):- 		% Indirect indexed - (IND), *y
	read(*pc,R) &&
	ab(R + 1,R ,R) &&
	R <- R + *y, *pc <= *pc + 1.

zpx(R):- 		% Zero page indexed by *x
	read(*pc,R1) && 
	R <- byte(R1 + *x), *pc <= *pc + 1.

zpy(R):- 		% Zero page indexed by *y
	read(*pc,R1) && 
	R <- byte(R1 + *y), *pc <= *pc + 1.

absy(R):- 		% absolute modified by *y
	ab(*pc + 1, *pc,R1) && 
	R <- R1 + *y , *pc <= *pc + 2.

absx(R) :- 		% absolute modified by *x
	ab(*pc + 1, *pc,R1) &&
	R <- R1 + *x , *pc <= *pc + 2.


% *SERVICE.FACILITIES

push(Dbb) :-			% Push a byte on the stack
	write(hex("100") + *s, Dbb),
	*s <= *s - 1.

pull(R):- 			% pull a byte off the stack
	*s <= *s + 1 &&
	read(hex("100") + *s,R).

opex :- 	 			% Operation exception
	*ready <= 0 && run.

setnz(Ta):-			% Set neg and zero condition code
	Ta = 0,!, *z <= 1, *n <= 0.
setnz(Ta):-	
	Ta < 0,!, *z <= 0, *n <= 1.
setnz(Ta):- 
	Ta > 0,!, *z <= 0, *n <= 0.

branch(0) :-  *pc <= *pc + 1.
branch(1) :-  read(*pc,R) && 
	*pc <= *pc + 1 + signed(R). % Relative addressing

decimal_adjust(Tac):-		% Used by sbc and adc
	( if (bit(7,*a) = bit(7,Tac))
	 then 
		*v <= bit(7,Tac) xor bit(7,*a),
		*c <= bit(8,Tac)  ) &&
	( if (*d = 1) then (
		(if Tac /\ binary("1111") > 9 then
			 Tac <- (Tac/\hex("ff") + 6)) &&
		(if *c = 0 then *c <= bit(8,Tac)) &&
		(if (Tac /\ binary("11110000")>>4) > 9 then
			 Tac <- (Tac/\hex("ff") + hex("60"))) &&
		(if *c = 0 then *c <= bit(8,Tac))
	)) &&
	*a <= byte(Tac) &&
	setnz(*a).

ab(Adh,Adl,R):-		% *address buffer
	read_2(Adh,Adl,R1,R2),
	fin( R = R1<<8 + R2 ).

% Read and write memory access routines

read(Adr,Value):-		% Read from valid memory
	*rw <= 1, Adr <- Adr &&
	read_1(Adr,Value).
read_1(Adr,Value):-
	*ready=0,!, int,Adr <- Adr && read_1(Adr,Value).
read_1(Adr,Value) :-
	Value <- *mem(Adr).

read_2(AdrH,AdrL,Vh,Vl) :-
	read(AdrH,Vh) && read(AdrL,Vl), Vh <- Vh.

write(Adr,Value) :-	% Write to valid memory
	*rw <=0,Adr <- Adr,Value <-Value &&
	*mem(Adr) <= Value.

% Interrupt routines

intstk :- 				% Interrupt stack operations
	push(high(*pc)) &&
	push(low(*pc)) &&
	push(*p), *i <= 1.

int :- 				% Interrupt processing
    *reset = 0,!,
    *reset <= 1,*irq <= 1,*nmi <= 1,*ready <= 1 &&
    ab(hex("FFFD"), hex("FFFC"),R) &&
    *pc <= R, *i <= 1.
int :-	
    *nmi = 0,!,
    *nmi <= 1 &&
    intstk &&
    ab(hex("FFFB"), hex("FFFA"),R) &&
    *pc <= R.
int :-	    
    (*b = 1 ; *irq = 0, *i =  0),!,
    intstk, *b <= 0 &&
    ab(hex("FFFF"), hex("FFFE"),R) &&
    *pc <= R.
int.

%  INSTRUCTION.INTERPRETATION
%      Yes It is the main routine.

run :-
    (if *reset = 0 then int ) &&		% Initial startup
	run1.
run1 :-	*ready = 0 ,! , empty.
run1 :- *ifsync <= 1 &&				% Instruction fetch
    read(*pc,R) &&
    *ir <= R , *pc <= *pc + 1, *ifsync <= 0 &&	% Execute
    run_decode(*ir/\binary("11")) &&
    int &&
    ( if *so=1 then *v <= 1), status_report && 
    run.
     
    run_decode(binary("01")) :- !, 
	    I1 = (*ir>>5)/\binary("111"),group1(I1).
    run_decode(binary("10")) :- !, 
	    I1 = (*ir>>5)/\binary("111"),group2(I1).
    run_decode(binary("00")) :- !, group3(*ir).
    run_decode(binary("11")) :- !, opex.

% Group 1 instruction decode

group1( 0 ):- ora.
group1( 1 ):- and.
group1( 2 ):- eor.
group1( 3 ):- adc.
group1( 4 ):- sta.
group1( 5 ):- lda.
group1( 6 ):- cmp.
group1( 7 ):- sbc.

% Group 2 instruction decode

group2( 0 ):- asl.
group2( 1 ):- rol.
group2( 2 ):- lsr.
group2( 3 ):- ror.
group2( 4 ):- stx.	    % Includes txa. txs
group2( 5 ):- ldx.	    % Includes tax. tsx
group2( 6 ):- dec.	    % Includes dex
group2( 7 ):- inc.	    % Includes no.op

% Group 3 instruction decode

group3(hex("00")) :- !, brk.	% Break
group3(hex("08")) :- !, php.	% push status on stack
group3(hex("28")) :- !, plp.	% pull status from stack
group3(hex("48")) :- !, pha.	% push accumulator
group3(hex("68")) :- !, pla.	% pull accumulator
group3(hex("10")) :- !, bpl.	% Branch on plus
group3(hex("30")) :- !, bmi.	% Branch on minus
group3(hex("50")) :- !, bvc.	% Branch if overflow clear
group3(hex("70")) :- !, bvs.	% Branch if overflow set
group3(hex("90")) :- !, bcc.	% Branch on carry clear
group3(hex("D0")) :- !, bne.	% Branch on not equal
group3(hex("F0")) :- !, beq.	% Branch if equal
group3(hex("B0")) :- !, bcs.	% Branch if carry set
group3(hex("18")) :- !, clc.	% Clear carry
group3(hex("38")) :- !, sec.	% set carry
group3(hex("58")) :- !, cli.	% Clear interrupt enable
group3(hex("78")) :- !, sei.	% set interrupt enable
group3(hex("B8")) :- !, clv.	% Clear overflow
group3(hex("D8")) :- !, cld.	% Clear decimal mode
group3(hex("F8")) :- !, sed.	% set decimal mode
group3(hex("20")) :- !, jsr.	% Jump to subroutine
group3(hex("24")) :- !, 	% Bit test - zero page
    zp(Adr) && read(Adr,V) && bit(V).
group3(hex("2C")) :- !, 	% Bit test - absolute
    abs(Adr) && read(Adr,V) && bit(V).
group3(hex("40")) :- !, rti.	% Return from interrupt
group3(hex("4C")) :- !, jmp.	% Jump - absolute
group3(hex("6C")) :- !, jmp.	% Jump - indirect
group3(hex("60")) :- !, rts.	% Return from subroutine
group3(hex("84")) :- !, 	% Store *y - zero page
    zp(Adr) && sty(Adr).
group3(hex("8C")) :- !, 	% Store *y - absolute
    abs(Adr) && sty(Adr).
group3(hex("94")) :- !, 	% Store *y - zero page, *x
    zpx(Adr) && sty(Adr).
group3(hex("88")) :- !, dey.	% Decrement *y
group3(hex("C8")) :- !, iny.	% Increment *y
group3(hex("E8")) :- !, inx.	% Increment *x
group3(hex("98")) :- !, tya.	% Transfer *y to *a
group3(hex("A8")) :- !, tay.	% Transfer *a to *y
group3(hex("A0")) :- !, 	% Load *y - immediate
    immed(Adr) && ldy(Adr).
group3(hex("A4")) :- !, 	% Load *y - zero page
    zp(Adr) && ldy(Adr).
group3(hex("AC")) :- !, 	% Load *y - absolute
    abs(Adr) && ldy(Adr).
group3(hex("B4")) :- !, 	% Load *y - zero page, *x
    zpx(Adr) && ldy(Adr).
group3(hex("BC")) :- !, 	% Load *y - absolute, *x
    absz(Adr) && ldy(Adr).
group3(hex("C0")) :- !, 	% Compare immediate to *y
    immed(Adr) && cpy(Adr).
group3(hex("C4")) :- !, 	% Compare zero page to *y
    zp(Adr) && cpy(Adr).
group3(hex("CC")) :- !, 	% Compare absolute to *y
    abs(Adr) && cpy(Adr).
group3(hex("E0")) :- !, 	% Compare immediate to *x
    immed(Adr) && cpx(Adr).
group3(hex("E4")) :- !, 	% Compare zero page to *x
    zp(Adr) && cpx(Adr).
group3(hex("EC")) :- !, 	% Compare absolute to *x
    abs(Adr) && cpx(Adr).
group3(I) :- opex.


% INSTRUCTION.EXECUTION

% Group 1 instruction execution

addrs1(Adr) :- 				% Group 1 address generation
    I =  (*ir >> 2 ) /\ binary("111"),
    addrs1(I,Adr).

addrs1( 0 , Adr):- indx(Adr).
addrs1( 1 , Adr):- zp(Adr).
addrs1( 2 , Adr):- immed(Adr).
addrs1( 3 , Adr):- abs(Adr).
addrs1( 4 , Adr):- indy(Adr).
addrs1( 5 , Adr):- zpx(Adr).
addrs1( 6 , Adr):- absy(Adr).
addrs1( 7 , Adr):- absx(Adr).

ora :- 						% Or
    addrs1(Adr) && read(Adr,R) && *a <= *a /\ R &&
    setnz(*a).

and :- 						% And
    addrs1(Adr) && read(Adr,R) && *a <= *a /\ R &&
    setnz(*a).

eor :- 						% Exclusive or
    addrs1(Adr) && read(Adr,R) && *a <= *a xor R &&
    setnz(*a).

adc :- 
    addrs1(Adr) && read(Adr,R) && 
    decimal_adjust(*a + *c + R).	% add with carry

sta :- *ir \= hex("89"),!,
    addrs1(Adr) && write(Adr,*a).	% store immediate

lda :- 						% Load accumulator
    addrs1(Adr) && read(Adr,R) && *a <= R &&
    setnz(*a).

    cmp :- 						% Compare
	addrs1(Adr) && read(Adr,R) && setnz(*a - R) &&
	if *a > R then *c<=1 else *c<=0.
 
    sbc :- 
	addrs1(Adr) && read(Adr,R) && 
	decimal_adjust(*a + *c - R).			% Sub/carry
 
    % Group 2 addressing mode selection
 
    % Group 2 gets and puts
 
    get2(R1,Adr) :- 	% Get the correct operand and return it in R1
	I = (*ir >> 2) /\ binary("111"),
	get2(I,R,Adr) ,fin( R1 = R + (*c << 8)).
	
        get2(1,R,Adr) :- zp(Adr)   && Adr <- Adr, read(Adr,R).
        get2(2,R,Adr) :- R <- *a, Adr <- Adr.
        get2(3,R,Adr) :- abs(Adr)  && Adr <- Adr, read(Adr,R).
        get2(5,R,Adr) :- zpx(Adr)  && Adr <- Adr, read(Adr,R).
        get2(7,R,Adr) :- absx(Adr) && Adr <- Adr, read(Adr,R).
	get2(_,R,Adr) :- opex.

    put2(Ta,Adr) :- 	% put the operand in the proper location
	I = (*ir >> 2) /\ binary("111"),
	put2(I,Ta,Adr),Ta<-Ta && setnz(Ta).
 
	put2(1,Ta,Adr) :- write(Adr, Ta).
	put2(3,Ta,Adr) :- write(Adr, Ta).
	put2(5,Ta,Adr) :- write(Adr, Ta).
	put2(7,Ta,Adr) :- write(Adr, Ta).
	put2(2,Ta,Adr) :- *a <= Ta.
	put2(_,Ta,Adr) :-opex.
 
    % Group 2 instruction execution
 
    asl :- 					% Arithmetic shift left
	get2(V,Adr) &&	
	V1 = V << 1,
	*c <= (V1 >> 8) /\ 1,put2(byte(V1),Adr).

    rol :- 					% rotate left
	get2(V,Adr) &&
	V1 = (V << 1)+ *c,
	*c <= (V1 >> 8) /\ 1,put2(byte(V1),Adr).
 
    lsr :- 					% Logical shift right
	get2(V,Adr) &&
	V1 = (V >> 1)/\ hex("7f") ,
	 *c <= V /\ 1, put2(byte(V1),Adr).
 
    ror :- 					% Rotate right
	get2(V,Adr) &&
	V1 = (V >> 1)/\ hex("7f") + ( (V /\ 1) << 8), 
	*c <= V /\ 1 , 	put2(byte(V1),Adr).
	
    stx :- 					% store index register
	I = (*ir>>2)/\binary("111"),
	stx(I,*x).
	    
	stx(1,X) :- zp(Adr) && write(Adr, X).
	stx(2,X) :- *a <= X.			% Txa
	stx(3,X) :- as(Adr) && write(Adr, X).
	stx(5,X) :- zpy(Adr) && write(Adr, X).
	stx(6,X) :- *s <= X.			% Txs
    	stx(_,_) :- opex.
 
    ldx :- 					% Load index register
	I = (*ir>>2)/\binary("111"),
	ldx(I,X) && *x <= X && setnz(*x).
	
	ldx(0,X) :- immed(Adr) && read(Adr,X).
	ldx(1,X) :- zp(Adr) && read(Adr,X).
	ldx(2,X) :- X <- *a.			% Tax
	ldx(3,X) :- abs(Adr) && read(Adr,X).
	ldx(4,X) :- opex.
	ldx(5,X) :- zpy(Adr) && read(Adr,X).
	ldx(6,X) :- X <- *s.			% Tsx
	ldx(7,X) :- absy(Adr) && read(Adr,X).
 
    dec :- 					% Decrement
	*ir = hex("CA"),!,			% Dex
		 X = *x - 1,*x <= X, setnz(X).
    dec :- get2(Value,Adr) && put2(Value - 1,Adr).

    inc :- 					% Increment
	*ir = hex("EA"),!.			% EA no.op
    inc :-	
	get2(Value,Adr) && put2(Value + 1,Adr).
 
    % Group 3 instruction execution
 
    brk :- 
	*ready <= 0.			%   for Debug
%	(*b <= 1, *pc <= *pc+1).	% Break
 
    php :- push(*p).		% push processor status on stack
    plp :- pull(A),*p <= A.	% pull processor status from stack
    pha :- push(*a).		% push accumulator on stack
    pla :- 			% pull accumulator from stack
	pull(A) && *a <= A, setnz(A).
 
    bpl :- boolNot(*n,B),branch(B).	% Branch on plus
    bmi :- bool(*n,B),branch(B).	% Branch on minus
    bvc :- boolNot(*v,B),branch(B).	% Branch on overflow clear
    bvs :- bool(*v,B),branch(B).	% Branch if overflow set
    bcc :- boolNot(*c,B),branch(B).	% Branch on carry clear
    bne :- boolNot(*z,B),branch(B).	% Branch if not equal
    beq :- bool(*z,B),branch(B).	% Branch on equal
    bcs :- bool(*c,B),branch(B).	% Branch on carry set
 
bool(1,1). bool(0,0).
boolNot(1,0). boolNot(0,1).

    clc :- *c <= 0.		% Clear carry flag
    sec :- *c <= 1.		% Set carry
    cli :- *i <= 0.		% Clear interrupt disable bit
    sei :- *i <= 1.		% Set interrupt disable status
    clv :- *v <= 0.		% Clear overflow
    cld :- *d <= 0.		% Clear decimal mode
    sed :- *d <= 1.		% Set decimal mode
 
    jsr :- 			% Jump to subroutine
	push(high(*pc + 1)) &&
	push(low(*pc + 1)) &&
	abs(Value) && *pc <= Value.
 
    bit(Ta) :-		% Bit test
	*n <= Ta, (if (Ta /\ *a)=0 then *z <= 1 else *z <= 0).
 
    rti :-			% Return from interrupt
	pull(P) && *p <= P &&
	pull(P) && *pc<= P &&
	pull(P) && *pc<= (P<<8)+ *pc, *b <= 0.
 
    jmp :- *ir = hex("6C"),!,
	abs(Value) && *pc <= Value &&
	abs(Value) && *pc <= Value .	% Indirect
    jmp :- abs(Value) && *pc <= Value.
		
 
    % Group 3 instruction execution (page 2)
 
    rts :- 				% return from subroutine
	pull(P) && *pc<= P &&
	pull(P) && *pc<= (P<<8)+ *pc &&
	*pc <= *pc+1.

    sty(X) :- write(X, *y).		% Store index *y in memory
 
    dey :- 				% Decrement index *y by one
	Y = *y - 1,*y <= Y, setnz(Y).
 
    tya :- 				% Transfer index *y to accumulator
	*a <= *y, setnz(*y).
 
    ldy(A) :- read(A,Value) && *y <= Value. 	% Load index *y with memory

    tay :- 			     	% Transfer accumulator to index *y
	*y <= *a, setnz(*a).
 
    cpy(A) :- 		     	% Compare memory and index *y
	read(A,Value) && setnz(*y - Value), 
	(if *y > Value then *c <= 1 else *c <= 0).
 
    iny :- 			     	% Increment index *y by one
	Y = *y + 1 , *y <= Y, setnz(*y).
 
    cpx(A) :- 			% Compare memory and index *x
	read(A,Value) && setnz(*x - Value), 
	(if *x > Value then *c <= 1 else *c <= 0).
 
    inx :- 				% Increment index *x by one
	X = *x + 1, *x <= X, setnz(*x).

% End of MC6502