|
|
|---|
|
|
|
|---|
Features for RV32EM, with big endian memory.
(feat-rv32em-be) → feat
Function:
(defun feat-rv32em-be nil (declare (xargs :guard t)) (let ((__function__ 'feat-rv32em-be)) (declare (ignorable __function__)) (make-feat :base (feat-base-rv32e) :endian (feat-endian-big) :m t)))
Theorem:
(defthm featp-of-feat-rv32em-be (b* ((feat (feat-rv32em-be))) (featp feat)) :rule-classes :rewrite)