Lines Matching refs:dst
246 (transfer (s1,s0) (dst::dstL, src::srcL) =
247 transfer (twrite s1 dst (tread s0 src), s0) (dstL, srcL))`;
250 (!dst src.tdecode hs (TLDR dst src) =
251 twrite hs (inR dst) (tread hs (inE src))) /\
252 (!dst src.tdecode hs (TSTR dst src) =
253 twrite hs (inE dst) (tread hs (inR src))) /\
254 (tdecode hs (TMOV dst src) =
255 twrite hs (inR dst) (tread hs (roc_2_exp src))) /\
256 (tdecode hs (TADD dst src1 src2) =
257 twrite hs (inR dst) (tread hs (roc_2_exp src1) + tread hs (roc_2_exp src2))) /\
258 (tdecode hs (TSUB dst src1 src2) =
259 twrite hs (inR dst) (tread hs (roc_2_exp src1) - tread hs (roc_2_exp src2))) /\
260 (tdecode hs (TRSB dst src1 src2) =
261 twrite hs (inR dst) (tread hs (roc_2_exp src2) - tread hs (roc_2_exp src1))) /\
262 (tdecode hs (TMUL dst src1 src2_reg) =
263 twrite hs (inR dst) (tread hs (roc_2_exp src1) * tread hs (roc_2_exp src2_reg))) /\
264 (tdecode hs (TAND dst src1 src2) =
265 twrite hs (inR dst) (tread hs (roc_2_exp src1) && tread hs (roc_2_exp src2))) /\
266 (tdecode hs (TORR dst src1 src2) =
267 twrite hs (inR dst) (tread hs (roc_2_exp src1) !! tread hs (roc_2_exp src2))) /\
268 (tdecode hs (TEOR dst src1 src2) =
269 twrite hs (inR dst) (tread hs (roc_2_exp src1) ?? tread hs (roc_2_exp src2))) /\
270 (tdecode hs (TLSL dst src2_reg src2_num) =
271 twrite hs (inR dst) (tread hs (roc_2_exp src2_reg) << w2n src2_num)) /\
272 (tdecode hs (TLSR dst src2_reg src2_num) =
273 twrite hs (inR dst) (tread hs (roc_2_exp src2_reg) >>> w2n src2_num)) /\
274 (tdecode hs (TASR dst src2_reg src2_num) =
275 twrite hs (inR dst) (tread hs (roc_2_exp src2_reg) >> w2n src2_num)) /\
276 (tdecode hs (TROR dst src2_reg src2_num) =
277 twrite hs (inR dst) (tread hs (roc_2_exp src2_reg) #>> w2n src2_num))