Lambda32 : Head over to this repo as it is an extension of the current project.

Processor

This repository presents a functional, but soon-to-be fully-realized model of a 32-bit processor developed entirely from first principles. A finite-state automaton (FSA) was used to model the processor. Then, sequential logical expressions were derived from said automaton. Future enhancements will include a formal specification and verification of the processor in TLA+/TLAPS. The end goal of this project is a practical, formally verified, Turing complete processor built on an FPGA.

In this repository, you will find:

• A Simulink file : Simulink is a MATLAB-based software for modeling and simulating systems and will need to be installed. The interactive version of the FSA was designed in Simulink and looks like this:

Abstract overview of the FSA

Detailed FSA of the Multiplier

Detailed FSA of the Adder

• An OmniGraffle file : OmniGraffle is a tool for building visual diagrams and can be installed here. The non-interactive FSA was designed in OmniGraffle and looks like this:

FSA of the Multiplier

FSA of the Adder

• TLA file : TLA+ is a language designed to model systems using basic mathematics. TLAPS is a system for writing and checking formal proofs for said model. TLA+ and TLAPS can be installed here. It looks something like this:

Mathematical expression for variable xR11

Sample proof that CMP32 is correct

TLA+ can easily convert to LaTeX

• PDF file : This file is the TLA+ specification in LaTeX form.

Specification of XOR and CMP in LaTeX

• processor.asm : This file will eventually conain the full processor written in x86_64 assembly. Although the final goal is to have a physical processor on an FPGA, it would be nice to have a software version of the processor for simulation. The entire processor model was designed in a way so that it would only need to use registers for its internal build. It only needs registers R8-R15 on the x86_64 architecture for storing model input/output variables, and floating point registers XMM0-XMM15 for storing its own 32-bit registers. Registers RAX, RBX, RCX, RDX, RSI and RDI on the x86_64 processor can be used for computing logic or as temporary storage units. This is not to say the processor does not use other sources of memory at all (like RAM or cache). The processor will use RAM or cache when fetching an instruction or executing a load/store instruction. What is meant here is that the algorithms used to build the processor only use x86_64 register memory.

• model.txt : This is a text file containing the logical expression that make up the model.

• scripts.js : This file contains some random JS scripts that help automate writing some logical expressions that otherwise would have been a laborious task doing it by hand.

The Instruction Set Architecture (ISA)

Every instruction is 64-bits wide and is identified and checked for format in the Decode stage of the processor.

BITS	0	1	2	3	4	5	6	7	8	9	10	11	12	13	14	15	16	17	18	19	20	21	22	23	24	25	26	27	28	29	30	31	32	33	34	35	36	37	38	39	40	41	42	43	44	45	46	47	48	49	50	51	52	53	54	55	56	57	58	59	60	61	62	63
INSTRUCTION	ICODE
mov rA,D(rB,rC,s)	0								rA					rB					rC					s				D																																PADDING
mov D(rB,rC,s),rA	1								rA					rB					rC					s				D																																PADDING
lea rA,D(rB,rC,s)	2								rA					rB					rC					s				D																																PADDING
mov rA,D(rB)	9								rA					rB					D																																PADDING
mov D(rB),rA	10								rA					rB					D																																PADDING
mov rA,rB	17								rA					rB					PADDING
movl rA,rB	18								rA					rB					PADDING
movle rA,rB	19								rA					rB					PADDING
movg rA,rB	20								rA					rB					PADDING
movge rA,rB	21								rA					rB					PADDING
move rA,rB	22								rA					rB					PADDING
movne rA,rB	23								rA					rB					PADDING
and rA,rB	24								rA					rB					PADDING
or rA,rB	25								rA					rB					PADDING
xor rA,rB	26								rA					rB					PADDING
shl rA,rB	27								rA					rB					PADDING
shr rA,rB	28								rA					rB					PADDING
sar rA,rB	29								rA					rB					PADDING
add rA,rB	30								rA					rB					PADDING
sub rA,rB	31								rA					rB					PADDING
mult rA,rB	32								rA					rB					PADDING
cmp rA,rB	33								rA					rB					PADDING
mov rA,imm	44								rA					IMMEDIATE																																PADDING
not rA	51								rA					PADDING
push rA	52								rA					PADDING
pop rA	53								rA					PADDING
int DISP	59								DISPLACEMENT								PADDING
call DEST	60								DESTINATION																																PADDING
jump DEST	61								DESTINATION																																PADDING
jumpl DEST	62								DESTINATION																																PADDING
jumple DEST	63								DESTINATION																																PADDING
jumpg DEST	64								DESTINATION																																PADDING
jumpge DEST	65								DESTINATION																																PADDING
jumpe DEST	66								DESTINATION																																PADDING
jumpne DEST	67								DESTINATION																																PADDING
ret	76								PADDING
hlt	77								PADDING
nop	78								PADDING

32 Registers Each 32-bits Wide

#	Name
0	RIP
1	RSP
2	RBP
3	RCF
4-31	R4, R5, ..., R31