行为

从rs1和rs2寄存器中读取内容，进行定点加法后回存到rd指定的寄存器中

形式化描述

(declare-const(regf Array (_ BitVec 64)))

;定义寄存器文件regf

(declare-const rs1 (_ BitVec 5))

(declare-const rs2 (_ BitVec 5))

(declare-const rd (_ BitVec 5))

;定义5比特寄存器索引

(declare-const sum (bvadd(select(regf, rs1), select(regf, rs2))))

;sum等于从regf的索引rs1, rs2读取定点数之和

(store(sum, regf, rd))

;将sum存储到regf索引为rd处

(assert(not(= (select(regf, rd)), sum)))

(check-sat)