gistfile1.txt

(define-register A 8)
(define-register X 8)
(define-register Y 8)
(define-register SP 8)
(define-register PC 16)

(define-register RES 8)

(define-register HALT 1)

(define-register N 1)
(define-register V 1)
(define-register B 1)
(define-register D 1)
(define-register I 1)
(define-register Z 1)
(define-register C 1)

(define-register DBWE 1)
(define-register DBDI 32)
(define-register DBADDR 10)

(define-register INSTR 32)

(define-ram DATA D 1024 32)

(define-transition
  fetch
  ;; also does write-back
  (set! (DATA B ADDR) DBADDR)
  (set! (DATA B WE) DBWE)
  (set! (DATA B DI) DBDI)

  (set! (DATA A WE) 0)
  (set! (DATA A ADDR) PC)
  (set! INSTR (: (DATA A) 0 32))

  (set-next execute))

(define-transition
  execute
  (set! (DATA B WE) 0)
  (set! DBWE (bv 0))
  (set! DBDI (bv 
               0 0 0 0 0 0 0 0
               0 0 0 0 0 0 0 0
               0 0 0 0 0 0 0 0
               0 0 0 0 0 0 0 0))

  (let OPCODE (: INSTR 0 6))
  (let IMM (: INSTR 6 22))
  (let AFLAG (: INSTR 22))

  (set! (DATA B ADDR) (: IMM 0 10))
  (set! DBADDR (: IMM 0 10))

  (let arg-val (cond AFLAG (: (DATA B) 0 8) (: IMM 0 8)))

  (set! PC (+ PC 1))
  (case OPCODE
    (0 0 0 0 0 0) (do (set! A arg-val) (set! RES arg-val)) ;; LDA
    (1 0 0 0 0 0) (do (set! X arg-val) (set! RES arg-val)) ;; LDX
    (0 1 0 0 0 0) (do (set! Y arg-val) (set! RES arg-val)) ;; LDY

    ;; STA
    (1 1 0 0 0 0) (do
                    (set! DBWE (bv 1))
                    (set! DBDI (append A (bv 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0)))
                    (set! RES A))
    ;; STX
    (0 0 1 0 0 0) (do
                    (set! DBWE (bv 1))
                    (set! DBDI (append X (bv 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0)))
                    (set! RES X))
    ;; STY
    (1 0 1 0 0 0) (do
                    (set! DBWE (bv 1))
                    (set! DBDI (append Y (bv 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0)))
                    (set! RES Y))

    (0 1 1 0 0 0) (do (set! X A) (set! RES A)) ;; TAX
    (1 1 1 0 0 0) (do (set! A X) (set! RES X)) ;; TXA
    (0 0 0 1 0 0) (do (set! Y A) (set! RES A)) ;; TAY
    (1 0 0 1 0 0) (do (set! A Y) (set! RES Y)) ;; TYA
    (0 1 0 1 0 0) (do (set! Y X) (set! RES X)) ;; TXY
    (1 1 0 1 0 0) (do (set! X Y) (set! RES Y)) ;; TYX

    (0 0 1 1 0 0) (do (let Xnext (+ X 1)) (set! X Xnext) (set! RES Xnext)) ;; INX
    (1 0 1 1 0 0) (do (let Ynext (+ Y 1)) (set! Y Ynext) (set! RES Ynext)) ;; INY
    (0 1 1 1 0 0) (do (let Anext (+ A 1)) (set! A Anext) (set! RES Anext)) ;; INA
    (1 1 1 1 0 0) (do (let Xnext (- X 1)) (set! X Xnext) (set! RES Xnext)) ;; DEX
    (0 0 0 0 1 0) (do (let Ynext (- Y 1)) (set! Y Ynext) (set! RES Ynext)) ;; DEY
    (1 0 0 0 1 0) (do (let Anext (- A 1)) (set! A Anext) (set! RES Anext)) ;; DEA

    ;; ADC
    (0 1 0 0 1 0) (do
                    ;; TODO: detect carry and set flag
                    (let Anext (+ A arg-val))
                    (set! A Anext)
                    (set! RES Anext))
    ;; SBC
    (1 1 0 0 1 0) (do
                    (let Anext (- A arg-val))
                    (set! A Anext)
                    (set! RES Anext))
    ;; BRK
    (0 0 1 0 1 0) (set! B 1)

    ;; BNE
    (1 0 1 0 1 0) (if (not (: Z 0))
                      (set! PC IMM))
    ;; BEQ
    (0 1 1 0 1 0) (if (: Z 0)
                      (set! PC IMM))

    ;; CPX
    (1 1 1 0 1 0) (if (= X arg-val)
                      (set! RES 1)
                      (set! RES 0))
    ;; CPY
    (0 0 0 1 1 0) (if (= Y arg-val)
                    (set! RES 1)
                    (set! RES 0))

    ;; CPA
    (1 0 0 1 1 0) (if (= A arg-val)
                      (set! RES 1)
                      (set! RES 0))
     
    )

  (if (= RES 0)
    (set! Z (bv 1))
    (set! Z (bv 0)))

  (set-next fetch))