Run-x86isa-fib32
- Signature
(run-x86isa-fib32 input start-address halt-address xrun-limit x86)
→
(mv * * x86)
Definitions and Theorems
Function: run-x86isa-fib32
(defun
run-x86isa-fib32
(input start-address
halt-address xrun-limit x86)
(declare (xargs :stobjs (x86)))
(declare (type (unsigned-byte 8) input)
(type (signed-byte 48) start-address)
(type (signed-byte 48) halt-address)
(type (unsigned-byte 50) xrun-limit))
(let
((__function__ 'run-x86isa-fib32))
(declare (ignorable __function__))
(if (zp input)
(mv t 0 x86)
(b* (((mv flg steps x86)
(x86isa-one-fib32-cosim (1- input)
start-address
halt-address xrun-limit x86))
((unless flg)
(cw "~% Mismatch found!~%")
(mv flg 0 x86))
(- (cw "Input: ~p0 Steps: ~p1 ~%"
input steps)))
(run-x86isa-fib32 (1- input)
start-address
halt-address xrun-limit x86)))))
