Data.SBV.Examples.BitPrecise.Legato

Mostek architecture

type Address

data Register

data Flag

type Value

type Bit

type Registers

type Flags

type Memory

data Mostek

type Extract a

type Program

Low-level operations

getReg

setReg

getFlag

setFlag

peek

poke

checkOverflow

checkOverflowCorrect

Instruction set

type Instruction

ldx

lda

clc

rorM

rorR

bcc

adc

dex

bne

end

Legato's algorithm in Haskell/SBV

legato

Verification interface

runLegato

type InitVals

initMachine

legatoIsCorrect

Verification

type Model

correctnessTheorem

C Code generation

legatoInC