system3mmu.smv

MODULE UART (proc, proc2UARTvalue, proc2UARTAddress)
VAR
	Rx : unsigned word [ 8 ]; -- byte from the outside
	Tx : array 0 .. 8 of unsigned word [ 8 ]; --array of bytes that is written from the internal memory
	uart2CPU : unsigned word [ 8 ]; -- the data the UART writes to the CPU
	uart2mem : unsigned word [ 8 ]; -- the data the UART writes to RAM (no DMA)
	uart2memValue : unsigned word [ 8 ]; -- external		
ASSIGN
	next (Tx[0]) :=
		case
			proc = write2UART & proc2UARTAddress = 0 : proc2UARTvalue;
			TRUE : (Tx[0]);
		esac;
	next (Tx[1]) :=
		case
			proc = write2UART & proc2UARTAddress = 1 : proc2UARTvalue;
			TRUE : (Tx[1]);
		esac;
	next (Tx[2]) :=
		case
			proc = write2UART & proc2UARTAddress = 2 : proc2UARTvalue;
			TRUE : (Tx[2]);
		esac;
	next (Tx[3]) :=
		case
			proc = write2UART & proc2UARTAddress = 3 : proc2UARTvalue;
			TRUE : (Tx[3]);
		esac;
	next (Tx[4]) :=
		case
			proc = write2UART & proc2UARTAddress = 4 : proc2UARTvalue;
			TRUE : (Tx[4]);
		esac;
	next (Tx[5]) :=
		case
			proc = write2UART & proc2UARTAddress = 5 : proc2UARTvalue;
			TRUE : (Tx[5]);
		esac;
	next (Tx[6]) :=
		case
			proc = write2UART & proc2UARTAddress = 6 : proc2UARTvalue;
			TRUE : (Tx[6]);
		esac;
	next (Tx[7]) :=
		case
			proc = write2UART & proc2UARTAddress = 7 : proc2UARTvalue;
			TRUE : (Tx[7]);
		esac;
	next (uart2CPU) :=
		case
			proc = read2UART : Rx;
			TRUE : Rx;
		esac;

		-- memory model
	-- the secure address is address 513 
MODULE PTE -- page table entry
VAR
	ptes : array 0 .. 4 of unsigned word [ 8 ]; -- valid, virtual page, modified, protection, page frame

MODULE MMU (proc, proc2memValue, pageNumber, proc2memAddress, mmu2mainValue)
VAR
	tlb : array 0 .. 8 of unsigned word [ 8 ];
	mem2read : 0 .. 8;
	ASSIGN
	next (tlb[0]) :=
		case
			proc = write : tlb[pageNumber];
			TRUE : tlb[0];
		esac;
		
	next (mmu2mainValue[0]) :=
		case
			proc = read & proc2memAddress = 0 | proc2memAddress = 32 & tlb[0] != 0uo8_0: tlb[0];
			 
			TRUE : 0uo8_0; -- respond void if data in TLB is void
		esac;
	
	next (mem2read) :=
		case
			proc = read & proc2memAddress = 0 | proc2memAddress = 32 & tlb[0] = 0uo8_0: proc2memAddress;
			 
			TRUE : mem2read;
		esac;
		
MODULE MEM (proc,  uart2memValue, mmu)
DEFINE
	secureAddress := 7;
VAR
	data : array 0 .. 16 of unsigned word [ 8 ];
	mem2proc : unsigned word [ 8 ];
ASSIGN
	next (mem2proc) :=
		case
			proc = read : data[mmu.mem2read];
			TRUE : mem2proc;
		esac;
	next (data[secureAddress]) :=
		case
			proc = write & mmu.pageNumber = secureAddress : mmu.tlb[mmu.pageNumber];
			TRUE : data[secureAddress];
		esac;
	next (data[0]) :=
		case
			proc = write & mmu.pageNumber = 0 : mmu.tlb[mmu.pageNumber];
			TRUE : data[secureAddress];
		esac;
MODULE main
VAR
	proc : {idle, read, write, read2UART, write2UART, setDMAaddress};
	data : array 0 .. 8 of unsigned word [ 8 ];
	pageNumber : 0 .. 7;
	proc2UARTAddress : 0 .. 7;
	proc2memAddress : 0..7; -- the data the CPU writes to memory
	
	proc2memValue : unsigned word [ 8 ]; -- the data the CPU writes to memory
	proc2UARTvalue : unsigned word [ 8 ]; -- the data the CPU writes to the UART	
	mmu : MMU (proc, proc2memValue, pageNumber, proc2memAddress, data);
	memory : MEM (proc, uart2mem, mmu);
	uart0 : UART (proc, proc2UARTvalue, proc2UARTAddress);
ASSIGN
--if we write to the UART then after a while it will appear on Tx
	LTLSPEC G proc = write2UART & proc2UARTAddress = 0 -> F (next (uart0.Tx[0]) =
	proc2UARTvalue)
	-- if we write to the UART but not to the secure memory, then the secure memory is constant
	LTLSPEC G (pageNumber != memory.secureAddress) -> G
	(memory.data[memory.secureAddress] = next (memory.data[memory.secureAddress]))