+ with m.If(a1.is_nan & b1.is_nan):
+ m.d.comb += Assert(z1.is_nan)
+ with m.Elif(a1.is_nan & ~b1.is_nan):
+ m.d.comb += Assert(z1.v == b1.v)
+ with m.Elif(b1.is_nan & ~a1.is_nan):
+ m.d.comb += Assert(z1.v == a1.v)
+ with m.Else():
+ isrhs = Signal()
+ # if a1 is negative and b1 isn't, then we should return b1
+ with m.If(a1.s != b1.s):
+ m.d.comb += isrhs.eq(a1.s > b1.s)
+ with m.Else():
+ # if they both have the same sign
+ gt = Signal()
+ m.d.comb += gt.eq(self.a[0:width-1] < self.b[0:width-1])
+ m.d.comb += isrhs.eq(gt ^ a1.s)
+
+ with m.If(self.opc == 0):
+ m.d.comb += Assert(z1.v ==
+ Mux(self.opc[0] ^ isrhs,
+ b1.v, a1.v))
+