Run-x86isa-fact
- Signature
(run-x86isa-fact input start-address
halt-address xrun-limit sys-view? x86)
→
(mv * x86)- Arguments
- sys-view? — Guard (booleanp sys-view?).
Definitions and Theorems
Function: run-x86isa-fact
(defun run-x86isa-fact (input start-address
halt-address xrun-limit sys-view? x86)
(declare (xargs :stobjs (x86)))
(declare (type (unsigned-byte 50) input)
(type (signed-byte 48) start-address)
(type (signed-byte 48) halt-address)
(type (unsigned-byte 50) xrun-limit))
(declare (xargs :guard (booleanp sys-view?)))
(let ((__function__ 'run-x86isa-fact))
(declare (ignorable __function__))
(if (zp input)
(mv t x86)
(b*
(((mv flg x86)
(x86isa-one-fact-cosim (1- input)
start-address
halt-address xrun-limit sys-view? x86))
((unless flg)
(cw "~% Mismatch found!~%")
(mv flg x86)))
(run-x86isa-fact (1- input)
start-address halt-address
xrun-limit sys-view? x86)))))
