/******************************************************************************
** FILE: sparc_v9.fs
** Facile description file for the SPARC v.9 instruction semantics.
** This file includes the SPARC v.9 encoding and register desriptions.
*/

#include "sparc_v9_enc.fs"
#include "sparc_v9_reg.fs"

extern save_regs(cwp_t,cwp_t) : void;
extern restore_regs(cwp_t) : void;

extern flush_windows(cwp_t,cwp_t) : void;
fun _flushw() {
    flush_windows(CWP,CANRESTORE);
    CANSAVE = (NWINDOWS - 2)?cvt(cwp_t);
    CANRESTORE = 0?cvt(cwp_t);
}
#define FLUSHW _flushw()

extern trap_sparc(ulong,cwp_t,cwp_t): void;
fun _trap(iflag,rs2,imm7) {
    val tnum;
    if(iflag) tnum = imm7?ext(32);
    else tnum = Rx(rs2)?cvt(ulong) & 0x7f?ext(32);

    if(tnum == 3) FLUSHW;
    else trap_sparc(tnum+256,CWP,CANRESTORE);
}
#define TRAP _trap(i,rs2,sw_trap)

#define TAG_OVERFLOW	0x23?ext(32)
#define INVALID		0x21?ext(32)

fun annul() {
    nPC = nPC2;
    nPC2 = nPC + 4;
}

fun get_src2(iflag,rs2,simm) {
    if(iflag) return simm?sext(64);
    else return Rx(rs2);
}

#define SRC2 get_src2(i,rs2,simm13)

//
// branch/call instructions

sem call {
    nPC2 = PC + disp30?sext(32)<<2;
    Rx(15,PC?addr?ext(64));
};

sem jmpl {
    nPC2 = (Rx(rs1) + SRC2)?cvt(stream);
    Rx(rd,PC?addr?ext(64));
};

sem retrn {
    nPC2 = (Rx(rs1) + SRC2)?cvt(stream);
    if(CANRESTORE?cvt(ulong) > 0) {
	CANSAVE = (CANSAVE?cvt(ulong) + 1)?cvt(cwp_t);
	CANRESTORE = (CANRESTORE?cvt(ulong) - 1)?cvt(cwp_t);
    } else {
	restore_regs(CWP);
	if(CANSAVE?cvt(ulong) < NWINDOWS-2)
	    CANSAVE = (CANSAVE?cvt(ulong) + 1)?cvt(cwp_t);
    }
    CWP = ((CWP?cvt(ulong) + NWINDOWS - 1) % NWINDOWS)?bits(5);
};

sem [ brz brlez brlz brnz brgz brgez ] {
    if(test(Rx(rs1),0?cvt(ullong)))
	nPC2 = PC + ((d16hi?sext(32)<<16) | (d16lo?ext(32)<<2));
    else if(a) annul();
} where test in [ == <= < != > >= ];

fun f_u(nn) { return fcc[nn]?bits(2) == 0b11; }
fun f_g(nn) { return fcc[nn]?bits(2) == 0b10; }
fun f_ug(nn) { return fcc[nn]?bit(1); }
fun f_l(nn) { return fcc[nn]?bits(2) == 0b01; }
fun f_ul(nn) { return fcc[nn]?bit(0); }
fun f_lg(nn) { val xx = fcc[nn]?bits(2); return xx==0b01 || xx==0b10; }
fun f_ne(nn) { return fcc[nn]?bits(2) != 0b00; }
fun f_e(nn) { return fcc[nn]?bits(2) == 0b00; }
fun f_ue(nn) { val xx = fcc[nn]?bits(2); return xx==0b00 || xx==0b11; }
fun f_ge(nn) { return !fcc[nn]?bit(0); }
fun f_uge(nn) { return fcc[nn]?bits(2) != 0b01; }
fun f_le(nn) { return !fcc[nn]?bit(1); }
fun f_ule(nn) { return fcc[nn]?bits(2) != 0b10; }
fun f_o(nn) { return fcc[nn]?bits(2) != 0b11; }

sem [ fba ba ] {
    nPC2 = PC + disp22?sext(32)<<2;
    if(a) annul();
};

sem [ fbpa bpa ] {
    nPC2 = PC + disp19?sext(32)<<2;
    if(a) annul();
};

sem [ fbn fbpn bn bpn ] { if(a) annul(); };

sem [			fbu	fbg	fbug	fbl	fbul	fblg
	fbne	fbe	fbue	fbge	fbuge	fble	fbule	fbo	] {
    if(cond(0)) nPC2 = PC + disp22?sext(32)<<2;
    else if(a) annul();
} where cond in [	f_u	f_g	f_ug	f_l	f_ul	f_lg
	f_ne	f_e	f_ue	f_ge	f_uge	f_le	f_ule	f_o	];

sem [			fbpu	fbpg	fbpug	fbpl	fbpul	fbplg
	fbpne	fbpe	fbpue	fbpge	fbpuge	fbple	fbpule	fbpo	] {
    if(cond(bpccr)) nPC2 = PC + disp19?sext(32)<<2;
    else if(a) annul();
} where cond in [	f_u	f_g	f_ug	f_l	f_ul	f_lg
	f_ne	f_e	f_ue	f_ge	f_uge	f_le	f_ule	f_o	];

#define C	CCR?bit(0)
#define V	CCR?bit(1)
#define Z	CCR?bit(2)
#define N	CCR?bit(3)
#define Cx	CCR?bit(4)
#define Vx	CCR?bit(5)
#define Zx	CCR?bit(6)
#define Nx	CCR?bit(7)

#define i_ne	(!Z)
#define i_e	(Z)
#define i_g	(!(Z|(N^V)))
#define i_le	(Z|(N^V))
#define i_ge	(!(N^V))
#define i_l	(N^V)
#define i_gu	(!(C|Z))
#define i_leu	(C|Z)
#define i_cc	(!C)
#define i_cs	(C)
#define i_pos	(!N)
#define i_neg	(N)
#define i_vc	(!V)
#define i_vs	(V)

#define x_ne	(!Zx)
#define x_e	(Zx)
#define x_g	(!(Zx|(Nx^Vx)))
#define x_le	(Zx|(Nx^Vx))
#define x_ge	(!(Nx^Vx))
#define x_l	(Nx^Vx)
#define x_gu	(!(Cx|Zx))
#define x_leu	(Cx|Zx)
#define x_cc	(!Cx)
#define x_cs	(Cx)
#define x_pos	(!Nx)
#define x_neg	(Nx)
#define x_vc	(!Vx)
#define x_vs	(Vx)

sem [			bne	be	bg	ble	bge	bl
	bgu	bleu	bcc	bcs	bpos	bneg	bvc	bvs	] {
    if(cond) nPC2 = PC + disp22?sext(32)<<2;
    else if(a) annul();
} where cond in [	i_ne	i_e	i_g	i_le	i_ge	i_l
	i_gu	i_leu	i_cc	i_cs	i_pos	i_neg	i_vc	i_vs	];

sem [			bpne	bpe	bpg	bple	bpge	bpl
	bpgu	bpleu	bpcc	bpcs	bppos	bpneg	bpvc	bpvs	] {
    if(bpcc1) {
	if(cond_xcc) nPC2 = PC + disp19?sext(32)<<2;
	else if(a) annul();
    } else if(cond_icc) nPC2 = PC + disp19?sext(32)<<2;
    else if(a) annul();
} where cond_xcc in [	x_ne	x_e	x_g	x_le	x_ge	x_l
	x_gu	x_leu	x_cc	x_cs	x_pos	x_neg	x_vc	x_vs	],
	cond_icc in [	i_ne	i_e	i_g	i_le	i_ge	i_l
	i_gu	i_leu	i_cc	i_cs	i_pos	i_neg	i_vc	i_vs	];

//
// Conditional moves:

sem [ fmovfsn fmovfdn fmovsn fmovdn] {};
sem [ fmovfsa fmovfda fmovsa fmovda ] { fd(rd,fs(rs2)); }
where fs in [ F4 F8 F4 F8 ], fd in [ F4 F8 F4 F8 ];

sem [					fmovsne		fmovse
	fmovsg		fmovsle		fmovsge		fmovsl
	fmovsgu		fmovsleu	fmovscc		fmovscs
	fmovspos	fmovsneg	fmovsvc		fmovsvs	] {
    if(bpcc1) { if(cond_xcc) F4(rd,F4(rs2)); }
    else if(cond_icc) F4(rd,F4(rs2));
} where cond_xcc in [	x_ne	x_e	x_g	x_le	x_ge	x_l
	x_gu	x_leu	x_cc	x_cs	x_pos	x_neg	x_vc	x_vs	],
	cond_icc in [	i_ne	i_e	i_g	i_le	i_ge	i_l
	i_gu	i_leu	i_cc	i_cs	i_pos	i_neg	i_vc	i_vs	];

sem [					fmovdne		fmovde
	fmovdg		fmovdle		fmovdge		fmovdl
	fmovdgu		fmovdleu	fmovdcc		fmovdcs
	fmovdpos	fmovdneg	fmovdvc		fmovdvs	] {
    if(bpcc1) { if(cond_xcc) F8(rd,F8(rs2)); }
    else if(cond_icc) F8(rd,F8(rs2));
} where cond_xcc in [	x_ne	x_e	x_g	x_le	x_ge	x_l
	x_gu	x_leu	x_cc	x_cs	x_pos	x_neg	x_vc	x_vs	],
	cond_icc in [	i_ne	i_e	i_g	i_le	i_ge	i_l
	i_gu	i_leu	i_cc	i_cs	i_pos	i_neg	i_vc	i_vs	];

sem [					fmovfsu		fmovfsg
	fmovfsug	fmovfsl		fmovfsul	fmovfslg
	fmovfsne	fmovfse		fmovfsue	fmovfsge
	fmovfsuge	fmovfsle	fmovfsule	fmovfso	] {
    if(cond(bpccr)) F4(rd,F4(rs2));
} where cond in [	f_u	f_g	f_ug	f_l	f_ul	f_lg
	f_ne	f_e	f_ue	f_ge	f_uge	f_le	f_ule	f_o	];

sem [					fmovfdu		fmovfdg
	fmovfdug	fmovfdl		fmovfdul	fmovfdlg
	fmovfdne	fmovfde		fmovfdue	fmovfdge
	fmovfduge	fmovfdle	fmovfdule	fmovfdo	] {
    if(cond(bpccr)) F8(rd,F8(rs2));
} where cond in [	f_u	f_g	f_ug	f_l	f_ul	f_lg
	f_ne	f_e	f_ue	f_ge	f_uge	f_le	f_ule	f_o	];

sem [ fmovrsz fmovrslez fmovrslz fmovrsnz fmovrsgz fmovrsgez ]
{ if(test(Rx(rs1),0?cvt(ullong))) F4(rd,F4(rs2)); }
where test in [ == <= < != > >= ];

sem [ fmovrdz fmovrdlez fmovrdlz fmovrdnz fmovrdgz fmovrdgez ]
{ if(test(Rx(rs1),0?cvt(ullong))) F8(rd,F8(rs2)); }
where test in [ == <= < != > >= ];

sem [ mova movfa ] { Rx(rd,Rx(rs2)); };
sem [ movn movfn ] {};

sem [					movne		move
	movg		movle		movge		movl
	movgu		movleu		movcc		movcs
	movpos		movneg		movvc		movvs	] {
    if(bpcc1) { if(cond_xcc) Rx(rd,Rx(rs2)); }
    else if(cond_icc) Rx(rd,Rx(rs2));
} where cond_xcc in [	x_ne	x_e	x_g	x_le	x_ge	x_l
	x_gu	x_leu	x_cc	x_cs	x_pos	x_neg	x_vc	x_vs	],
	cond_icc in [	i_ne	i_e	i_g	i_le	i_ge	i_l
	i_gu	i_leu	i_cc	i_cs	i_pos	i_neg	i_vc	i_vs	];

sem [			movfu	movfg	movfug	movfl	movful	movflg
	movfne	movfe	movfue	movfge	movfuge	movfle	movfule	movfo	] {
    if(cond(bpccr)) Rx(rd,Rx(rs2));
} where cond in [	f_u	f_g	f_ug	f_l	f_ul	f_lg
	f_ne	f_e	f_ue	f_ge	f_uge	f_le	f_ule	f_o	];

sem [ movrz movrlez movrlz movrnz movrgz movrgez ]
{ if(test(Rx(rs1),0?cvt(ullong))) Rx(rd,Rx(rs2)); }
where test in [ == <= < != > >= ];

//
// System traps:

sem ta { TRAP; };
sem tn {};

sem [			tne	te	tg	tle	tge	tl
	tgu	tleu	tcc	tcs	tpos	tneg	tvc	tvs	] {
    if(bpcc1) { if(cond_xcc) TRAP; }
    else if(cond_icc) TRAP;
} where cond_xcc in [	x_ne	x_e	x_g	x_le	x_ge	x_l
	x_gu	x_leu	x_cc	x_cs	x_pos	x_neg	x_vc	x_vs	],
	cond_icc in [	i_ne	i_e	i_g	i_le	i_ge	i_l
	i_gu	i_leu	i_cc	i_cs	i_pos	i_neg	i_vc	i_vs	];

//
// Arithmetic ops:

#define C64 (CCR?bit(0)?ext(64))

sem [ add sub and or xor ]
{ Rx(rd, op(Rx(rs1),SRC2)); }
where op in [ + - & | ^ ];

sem [ addcc subcc andcc orcc xorcc ]
{ Rx(rd, op(Rx(rs1),SRC2)?cc(CCR)); }
where op in [ + - & | ^ ];

sem addc { Rx(rd, Rx(rs1) + SRC2 + C64); };
sem subc { Rx(rd, Rx(rs1) - SRC2 - C64); };

sem addccc {
    val ccr = 0x00?cvt(cc);
    val x1 = Rx(rs1); val x2 = SRC2;
    val xx = ((x1 + x2)?cc(ccr) + C64)?cc(CCR);
    CCR = ((CCR?bits(8) & 0b11011101) | (ccr?bits(8) & 0x11) |
	   (((x1?bit(31)==x2?bit(31))&&(xx?bit(31)!=x1?bit(31)))?ext(8)<<1) |
	   (((x1?bit(63)==x2?bit(63))&&(xx?bit(63)!=x1?bit(63)))?ext(8)<<5))
	? cvt(cc);
    Rx(rd, xx);
};

sem subccc {
    val ccr = 0x00?cvt(cc);
    val x1 = Rx(rs1); val x2 = SRC2;
    val xx = ((x1 - x2)?cc(ccr) - C64)?cc(CCR);
    CCR = ((CCR?bits(8) & 0b11011101) | (ccr?bits(8) & 0x11) |
	   (((x1?bit(31)!=x2?bit(31))&&(xx?bit(31)!=x1?bit(31)))?ext(8)<<1) |
	   (((x1?bit(63)!=x2?bit(63))&&(xx?bit(63)!=x1?bit(63)))?ext(8)<<5))
	? cvt(cc);
    Rx(rd, xx);
};

sem [ andn orn xnor ] { Rx(rd, op(Rx(rs1),~SRC2)); } where op in [ & | ^ ];

sem [ andncc orncc xnorcc ]
{ Rx(rd, op(Rx(rs1),~SRC2)?cc(CCR)); }
where op in [ & | ^ ];

sem [ mulx udivx ] { Rx(rd,  op(Rx(rs1),SRC2)); } where op in [ * / ];
sem sdivx { Rx(rd,(+Rx(rs1) / +SRC2)?cast(ullong)); };

sem sll		{ Rx(rd,  Rx(rs1) << SRC2?bits(5)); };
sem srl		{ R4(rd,  R4(rs1) >> SRC2?bits(5)); };
sem sra		{ Rx(rd,(+R4(rs1) >> SRC2?bits(5))?sext(64)); };
sem sllx	{ Rx(rd,  Rx(rs1) << SRC2?bits(6)); };
sem srlx	{ Rx(rd,  Rx(rs1) >> SRC2?bits(6)); };
sem srax	{ Rx(rd,(+Rx(rs1) >> SRC2?bits(6))?cast(ullong)); };

sem taddcc {
    val x1 = Rx(rs1); val x2 = SRC2;
    Rx(rd, (x1 + x2)?cc(CCR));
    if(x1?bits(2)!=0b00 || x2?bits(2)!=0b00)
	CCR = (CCR?bits(8) | 0x02)?cvt(cc);
};

sem taddcctv {
    val x1 = Rx(rs1); val x2 = SRC2;
    Rx(rd, (x1 + x2)?cc(CCR));
    if(x1?bits(2)!=0b00 || x2?bits(2)!=0b00)
	CCR = (CCR?bits(8) | 0x02)?cvt(cc);
    if(CCR?bit(1)) trap_sparc(TAG_OVERFLOW,CWP,CANRESTORE);
};

sem tsubcc {
    val x1 = Rx(rs1); val x2 = SRC2;
    Rx(rd, (x1 - x2)?cc(CCR));
    if(x1?bits(2)!=0b00 || x2?bits(2)!=0b00)
	CCR = (CCR?bits(8) | 0x02)?cvt(cc);
};

sem tsubcctv {
    val x1 = Rx(rs1); val x2 = SRC2;
    Rx(rd, (x1 - x2)?cc(CCR));
    if(x1?bits(2)!=0b00 || x2?bits(2)!=0b00)
	CCR = (CCR?bits(8) | 0x02)?cvt(cc);
    if(CCR?bit(1)) trap_sparc(TAG_OVERFLOW,CWP,CANRESTORE);
};

fun u_div32(x1,x2,var ccr) {
    val xx = x1 / x2?ext(64);
    if(xx > 1?ext(64)<<32) { xx = 0xffffffff?ext(64); ccr = ccr | 0x02; }
    return xx;
}

fun s_div32(x1,x2,var ccr) {
    val xx = (+x1 / +x2?sext(64))?cast(ullong);
    if(+xx > +(1?ext(64)<<31)) { xx = 0x7fffffff?ext(64); ccr = ccr | 0x02; }
    else if(+xx < +((-1)?sext(64)<<31)) {
	xx = 0x80000000?sext(64);
	ccr = ccr | 0x02;
    }
    return xx;
}

sem [ udiv sdiv ] {
    val ccr = 0x00;
    val xx = ((Y?ext(64)<<32) | R4(rs1)?ext(64));
    if(i) xx = _div(xx,simm13?sext(32)?ext(64),ccr);
    else xx = _div(xx,R4(rs2)?ext(64),ccr);
    Rx(rd,xx);
} where _div in [u_div32 s_div32];

sem umul {
    val xx = (Rx(rs1)&0xffffffff?ext(64)) * (SRC2&0xffffffff?ext(64)); 
    Y = (xx >> 32)?bits(32); R4(rd,xx?bits(32));
};

sem smul {
    val xx = +Rx(rs1)?bits(32)?sext(64) * +SRC2?bits(32)?sext(64);
    Y = (xx >> 32)?bits(32); R4(rd,xx?bits(32));
};

fun get_div_mul_cc(xx,ccr0) {
    val ccr = ccr0 | xx?bit(63)?ext(8) << 7;
    ccr = ccr | (xx==0?ext(64))?ext(8) << 6;
    ccr = ccr | xx?bit(31)?ext(8) << 3;
    return ccr | (xx?bits(32)==0)?ext(8) << 2;
}

sem [ udivcc sdivcc ] {
    val ccr = 0x00;
    val xx = ((Y?ext(64)<<32) | R4(rs1)?ext(64));
    if(i) xx = _div(xx,simm13?sext(32),ccr);
    else xx = _div(xx,R4(rs2),ccr);
    CCR = get_div_mul_cc(xx,ccr)?cvt(cc);
    Rx(rd,xx);
} where _div in [u_div32 s_div32];

sem umulcc {
    val xx = (Rx(rs1)&0xffffffff?ext(64)) * (SRC2&0xffffffff?ext(64)); 
    CCR = get_div_mul_cc(xx,0x00)?cvt(cc);
    Y = (xx >> 32)?bits(32); R4(rd,xx?bits(32));
};

sem smulcc {
    val xx = (+Rx(rs1)?bits(32)?sext(64) *
	      +SRC2?bits(32)?sext(64))?cast(ullong);
    CCR = get_div_mul_cc(xx,0x00)?cvt(cc);
    Y = (xx >> 32)?bits(32); R4(rd,xx?bits(32));
};

sem mulscc {
    val y0 = Y?bit(0); Y = (Y>>1) | (R4(rs1)?bit(0)?ext(32)<<31);
    val xx = (R4(rs1)>>1) | ((CCR?bit(3)^CCR?bit(1))?ext(32)<<31);
    if(y0) R4(rd, (xx + SRC2?bits(32))?cc(CCR));
    else R4(rd,(xx+0)?cc(CCR));
};

sem popc {
    val xx = Rx(rs2);
    val ii=0; val count=0?ext(64);
    while(ii < 64) {
	count = count + ((xx >> ii) & 0x1?ext(64));
	ii = ii + 1;
    }
    Rx(rd,count);
};

sem flush {};
sem flushw { FLUSHW; };

sem rd {
    switch(rs1?ext(32)) {
     case 0:	Rx(rd,Y?ext(64));
     case 2:	Rx(rd,CCR?bits(8)?ext(64));
     case 5:	Rx(rd,PC?addr?ext(64));
     case 15:	assert(rd?ext(32)==0);
     default:
	/* not implemented */
	assert(false);
    }
};

sem wr {
    switch(rd?ext(32)) {
     case 0:	Y = (Rx(rs1) ^ SRC2)?bits(32);
     case 2:	CCR = (Rx(rs1) ^ SRC2)?cvt(cc);
     default:
	/* not implemented */
	assert(false);
    }
};

sem save {
    val xx = Rx(rs1) + SRC2;
    if(CANSAVE?cvt(ulong) <= 0) {
	save_regs(CWP,CANRESTORE);
	CANSAVE = CANRESTORE; CANRESTORE = 0?cvt(cwp_t);
    }
    CWP = ((CWP?cvt(ulong) + 1) % NWINDOWS)?bits(5);
    CANSAVE = (CANSAVE?cvt(ulong) - 1)?cvt(cwp_t);
    CANRESTORE = (CANRESTORE?cvt(ulong) + 1)?cvt(cwp_t);
    Rx(rd,xx);
};

sem restore {
    val xx = Rx(rs1) + SRC2;
    if(CANRESTORE?cvt(ulong) > 0) {
	CANSAVE = (CANSAVE?cvt(ulong) + 1)?cvt(cwp_t);
	CANRESTORE = (CANRESTORE?cvt(ulong) - 1)?cvt(cwp_t);
    } else {
	restore_regs(CWP);
	if(CANSAVE?cvt(ulong) < NWINDOWS-2)
	    CANSAVE = (CANSAVE?cvt(ulong) + 1)?cvt(cwp_t);
    }
    CWP = ((CWP?cvt(ulong) + NWINDOWS - 1) % NWINDOWS)?bits(5);
    Rx(rd,xx);
};

sem sethi { Rx(rd,imm22?ext(64)<<10); };

//
// Floating-point arithmetic:

sem [ fadds fsubs fmuls fdivs ]
{ F4(rd, op(F4(rs1),F4(rs2))); }
where op in [ + - * / ];

sem [ faddd fsubd fmuld fdivd ]
{ F8(rd, op(F8(rs1),F8(rs2))); }
where op in [ + - * / ];

sem [ fcmps fcmpd ] { (f(rs1)-f(rs2))?cc(fcc[cond]); } where f in [F4 F8];
sem [ fcmpes fcmped ] {
    (f(rs1)-f(rs2))?cc(fcc[cond]);
    if(f_u(cond)) trap_sparc(INVALID,CWP,CANRESTORE);
} where f in [F4 F8];

sem fstox { F8(rd,F4(rs2)?cvt(llong)?cast(ullong)); };
sem fdtox { F8(rd,F8(rs2)?cvt(llong)?cast(ullong)); };
sem fstoi { F4(rd,F4(rs2)?cvt(long)?cast(ulong)); };
sem fdtoi { F4(rd,F8(rs2)?cvt(long)?cast(ulong)); };
sem fstod { F8(rd,F4(rs2)?cvt(double)); };
sem fxtos { F4(rd,F8(rs2)?cast(llong)?cvt(float)); };
sem fxtod { F8(rd,F8(rs2)?cast(llong)?cvt(double)); };
sem fitos { F4(rd,F4(rs2)?cast(long)?cvt(float)); };
sem fitod { F8(rd,F4(rs2)?cast(long)?cvt(double)); };
sem fdtos { F4(rd,F8(rs2)?cvt(float)); };

sem [ fmovs fmovd ] { fd(rd,fs(rs2)); } where fs in [F4 F8], fd in [F4 F8];
sem [ fnegs fnegd ] { fd(rd,-fs(rs2)); } where fs in [F4 F8], fd in [F4 F8];
sem [ fabss fabsd ] { if(fs(rs2)<z) fd(rd,-fs(rs2)); else fd(rd,fs(rs2)); }
where fs in [F4 F8], fd in [F4 F8], z in [ (0?cvt(float)) (0?cvt(double)) ];

sem fsmuld { F8(rd, F4(rs1)?cvt(double) * F4(rs2)?cvt(double)); };

sem [fsqrts fsqrtd] {fd(rd,sqrt(fs(rs2)));} where fs in [F4 F8], fd in [F4 F8];

//
// Load, store, etc.:

sem [			ldf	lddf		ldfa	lddfa
	ldsb	ldsh	ldsw	ldub	lduh	lduw	ldx	ldd
	ldsba	ldsha	ldswa	lduba	lduha	lduwa	ldxa	ldda	] {
    r(rd, m(Rx(rs1) + SRC2));
} where r in [		F4	F8		F4	F8
	Rx	Rx	Rx	Rx	Rx	Rx	Rx	R8
	Rx	Rx	Rx	Rx	Rx	Rx	Rx	R8	],
	m in [		M4	M8		M4	M8
	M1s	M2s	M4s	M1	M2	M4	M8	M8
	M1s	M2s	M4s	M1	M2	M4	M8	M8	];

sem [		stf	stdf	stb	sth	stw	stx	std
		stfa	stdfa	stba	stha	stwa	stxa	stda	] {
    m(Rx(rs1) + SRC2, r(rd));
} where r in [	F4	F8	Rx	Rx	Rx	Rx	R8
		F4	F8	Rx	Rx	Rx	Rx	R8	],
	m in [	M4	M8	M1	M2	M4	M8	M8
		M4	M8	M1	M2	M4	M8	M8	];

sem [ casa casxa ] {
    val aa = Rx(rs1); val xx = ms(aa);
    if(rsrc(rs2)?ext(64) == xx) md(aa,rsrc(rd)); rdest(rd,xx);
} where rsrc in [R4 Rx], rdest in [R4 Rx],
	ms in [M4 M8], md in [M4 M8];

sem [ ldstub ldstuba ] { val aa=Rx(rs1)+SRC2; Rx(rd,M1(aa)); M1(aa,0xff); };

sem [ prefetch prefetcha ] {};

sem [ swap swapa ] {
    val aa = Rx(rs1) + SRC2; val xx = M4(aa);
    M4(aa,R4(rd)); R4(rd,xx);
};

sem ldfsr { set_FSR4(M4(Rx(rs1) + SRC2)?bits(32)); };
sem ldxfsr { set_FSR8(M8(Rx(rs1) + SRC2)); };
sem [ stfsr stxfsr ] { m(Rx(rs1) + SRC2, r()); }
where r in [ get_FSR4 get_FSR8 ], m in [ M4 M8 ];