Skip to content

Commit

Permalink
Improve provisos on FixedPoint function epsilon
Browse files Browse the repository at this point in the history
The epsilon function doesn't make sense for FixedPoint#(1,0), so
add provisos to forbid it
  • Loading branch information
darius-bluespec authored and quark17 committed Oct 24, 2023
1 parent 35b7f41 commit 48cb127
Showing 1 changed file with 10 additions and 1 deletion.
11 changes: 10 additions & 1 deletion src/Libraries/Base3-Math/FixedPoint.bsv
Original file line number Diff line number Diff line change
Expand Up @@ -150,7 +150,12 @@ endinstance

//@ \index{epsilon@\te{epsilon} (fixed-point function)|textbf}
//@ # 1
function FixedPoint#(i,f) epsilon () ;
function FixedPoint#(i,f) epsilon ()
provisos(
Min#(i,1,1),
Min#(TAdd#(i,f),2,2)
);

Int#(b) eps = 'b01 ;
return _fromInternal (eps);
endfunction
Expand All @@ -164,6 +169,7 @@ instance Arith#( FixedPoint#(i,f) )
provisos( Add#(i,f,b)
,Add#(TAdd#(i,i), TAdd#(f,f), TAdd#(b,b))
,Min#(i,1,1)
,Min#(TAdd#(i, f), 2, 2)
);

// Addition does not change the binary point
Expand Down Expand Up @@ -436,6 +442,7 @@ function FixedPoint#(ri,rf) fxptTruncateSat (SaturationMode smode, FixedPoint#(a
,Add#(rf,_f,af)
,Min#(ai,1,1)
,Min#(ri,1,1)
,Min#(TAdd#(ri, rf), 2, 2)
);

FixedPoint#(ri,rf) res = fxptTruncate(din);
Expand Down Expand Up @@ -473,6 +480,7 @@ function FixedPoint#(ri,rf) fxptTruncateRound (RoundMode rmode, FixedPoint#(ai,a
,Add#(rf,fdrop,af)
,Min#(ai,1,1)
,Min#(ri,1,1)
,Min#(TAdd#(ri, rf), 2, 2)
);
return fxptTruncateRoundSat(rmode, Sat_Wrap, din);
endfunction
Expand All @@ -483,6 +491,7 @@ function FixedPoint#(ri,rf) fxptTruncateRoundSat (RoundMode rmode, SaturationMod
,Add#(rf,fdrop,af)
,Min#(ai,1,1)
,Min#(ri,1,1)
,Min#(TAdd#(ri, rf), 2, 2)
);
Bit#(n) msbMask = (~('b0)) >> 1; // 'b011111...

Expand Down

0 comments on commit 48cb127

Please sign in to comment.