Term-level hzToPeriod has different behaviour than type-level Div
#1253
Comments
DigitalBrains1
added a commit
that referenced
this issue
Feb 10, 2021
This change does not significantly affect the generated circuit, although the change is observable in simulation. We would like `hzToPeriod` to satisfy the following: - Results should be intuitive - Results should match a type-level equivalent as proposed in issue #1253 #1253 The former can be done with `Double`, by rounding to the nearest integer. This means that if there is an exact integer solution, we give that. Before this commit we had: >>> hzToPeriod 100_000 10000001 instead of the intuitive result that a 100 MHz clock corresponds to a 10 ns period. The off-by-one has no significant consequences for the circuit, clocks are inherently not precise. It is just not intuitive. But if we also want the result to match a simply expressed type-level equivalent, this is not enough, because the slight errors introduced by `Double` might cause a fractional part of 0.5 to be rounded either up or down seemingly randomly. So the most straight-forward fix is to use `Ratio Natural` and `floor`. If the result is an integral number of picoseconds, it will give that, and for roundings, it will match the behaviour of the straightforward type-level equivalent of: type HzToPeriod (freq :: Nat) = 1_000_000_000_000 `Div` freq
DigitalBrains1
added a commit
that referenced
this issue
Feb 10, 2021
This change does not significantly affect the generated circuit, although the change is observable in simulation. We would like `hzToPeriod` to satisfy the following: - Results should be intuitive - Results should match a type-level equivalent as proposed in issue #1253 #1253 The former can be done with `Double`, by rounding to the nearest integer. This means that if there is an exact integer solution, we give that. Before this commit we had: >>> hzToPeriod 100_000 10000001 instead of the intuitive result that a 100 MHz clock corresponds to a 10 ns period. The off-by-one has no significant consequences for the circuit, clocks are inherently not precise. It is just not intuitive. But if we also want the result to match a simply expressed type-level equivalent, this is not enough, because the slight errors introduced by `Double` might cause a fractional part of 0.5 to be rounded either up or down seemingly randomly. So the most straightforward fix is to use `Ratio Natural` and `floor`. If the result is an integral number of picoseconds, it will give that, and for roundings, it will match the behaviour of the straightforward type-level equivalent of: type HzToPeriod (freq :: Nat) = 1_000_000_000_000 `Div` freq
DigitalBrains1
added a commit
that referenced
this issue
Feb 11, 2021
This change does not significantly affect the generated circuit, although the change is observable in simulation. We would like `hzToPeriod` to satisfy the following: - Results should be intuitive - Results should match a type-level equivalent as proposed in issue #1253 #1253 The former can be done with `Double`, by rounding to the nearest integer. This means that if there is an exact integer solution, we give that. Before this commit we had: >>> hzToPeriod 100_000 10000001 instead of the intuitive result that a 100 kHz clock corresponds to a 10 µs period. The off-by-one has no significant consequences for the circuit, clocks are inherently not precise. It is just not intuitive. But if we also want the result to match a simply expressed type-level equivalent, this is not enough, because the slight errors introduced by `Double` might cause a fractional part of 0.5 to be rounded either up or down seemingly randomly. So the most straightforward fix is to use `Ratio Natural` and `floor`. If the result is an integral number of picoseconds, it will give that, and for roundings, it will match the behaviour of the straightforward type-level equivalent of: type HzToPeriod (freq :: Nat) = 1_000_000_000_000 `Div` freq
DigitalBrains1
added a commit
that referenced
this issue
Feb 11, 2021
This change does not significantly affect the generated circuit, although the change is observable in simulation. We would like `hzToPeriod` to satisfy the following: - Results should be intuitive - Results should match a type-level equivalent as proposed in issue #1253 #1253 The former can be done with `Double`, by rounding to the nearest integer. This means that if there is an exact integer solution, we give that. Before this commit we had: >>> hzToPeriod 100_000 10000001 instead of the intuitive result that a 100 kHz clock corresponds to a 10 µs period. The off-by-one has no significant consequences for the circuit, clocks are inherently not precise. It is just not intuitive. But if we also want the result to match a simply expressed type-level equivalent, this is not enough, because the slight errors introduced by `Double` might cause a fractional part of 0.5 to be rounded either up or down seemingly randomly. So the most straightforward fix is to use `Ratio Natural` and `floor`. If the result is an integral number of picoseconds, it will give that, and for roundings, it will match the behaviour of the straightforward type-level equivalent of: type HzToPeriod (freq :: Nat) = 1_000_000_000_000 `Div` freq
DigitalBrains1
added a commit
that referenced
this issue
Feb 11, 2021
This change does not significantly affect the generated circuit, although the change is observable in simulation. We would like `hzToPeriod` to satisfy the following: - Results should be intuitive - Results should match a type-level equivalent as proposed in issue #1253 #1253 The former can be done with `Double`, by rounding to the nearest integer. This means that if there is an exact integer solution, we give that. Before this commit we had: >>> hzToPeriod 100_000 10000001 instead of the intuitive result that a 100 kHz clock corresponds to a 10 µs period. The off-by-one has no significant consequences for the circuit, clocks are inherently not precise. It is just not intuitive. But if we also want the result to match a simply expressed type-level equivalent, this is not enough, because the slight errors introduced by `Double` might cause a fractional part of 0.5 to be rounded either up or down seemingly randomly. So the most straightforward fix is to use `Ratio Natural` and `floor`. If the result is an integral number of picoseconds, it will give that, and for roundings, it will match the behaviour of the straightforward type-level equivalent of: type HzToPeriod (freq :: Nat) = 1_000_000_000_000 `Div` freq
DigitalBrains1
added a commit
that referenced
this issue
Feb 11, 2021
This change does not significantly affect the generated circuit, although the change is observable in simulation. We would like `hzToPeriod` to satisfy the following: - Results should be intuitive - Results should match a type-level equivalent as proposed in issue #1253 #1253 The former can be done with `Double`, by rounding to the nearest integer. This means that if there is an exact integer solution, we give that. Before this commit we had: >>> hzToPeriod 100_000 10000001 instead of the intuitive result that a 100 kHz clock corresponds to a 10 µs period. The off-by-one has no significant consequences for the circuit, clocks are inherently not precise. It is just not intuitive. But if we also want the result to match a simply expressed type-level equivalent, this is not enough, because the slight errors introduced by `Double` might cause a fractional part of 0.5 to be rounded either up or down seemingly randomly. So the most straightforward fix is to use `Ratio Natural` and `floor`. If the result is an integral number of picoseconds, it will give that, and for roundings, it will match the behaviour of the straightforward type-level equivalent of: type HzToPeriod (freq :: Nat) = 1_000_000_000_000 `Div` freq
DigitalBrains1
added a commit
that referenced
this issue
Feb 12, 2021
This change does not significantly affect the generated circuit, although the change is observable in simulation. We would like `hzToPeriod` to satisfy the following: - Results should be intuitive - Results should match a type-level equivalent as proposed in issue #1253 #1253 The former can be done with `Double`, by rounding to the nearest integer. This means that if there is an exact integer solution, we give that. Before this commit we had: >>> hzToPeriod 100_000 10000001 instead of the intuitive result that a 100 kHz clock corresponds to a 10 µs period. The off-by-one has no significant consequences for the circuit, clocks are inherently not precise. It is just not intuitive. But if we also want the result to match a simply expressed type-level equivalent, this is not enough, because the slight errors introduced by `Double` might cause a fractional part of 0.5 to be rounded either up or down seemingly randomly. So the most straightforward fix is to use `Ratio Natural` and `floor`. If the result is an integral number of picoseconds, it will give that, and for roundings, it will match the behaviour of the straightforward type-level equivalent of: type HzToPeriod (freq :: Nat) = 1_000_000_000_000 `Div` freq
DigitalBrains1
added a commit
that referenced
this issue
Feb 13, 2021
This change does not significantly affect the generated circuit, although the change is observable in simulation. We would like `hzToPeriod` to satisfy the following: - Results should be intuitive - Results should match a type-level equivalent as proposed in issue #1253 #1253 The former can be done with `Double`, by rounding to the nearest integer. This means that if there is an exact integer solution, we give that. Before this commit we had: >>> hzToPeriod 100_000 10000001 instead of the intuitive result that a 100 kHz clock corresponds to a 10 µs period. The off-by-one has no significant consequences for the circuit, clocks are inherently not precise. It is just not intuitive. But if we also want the result to match a simply expressed type-level equivalent, this is not enough, because the slight errors introduced by `Double` might cause a fractional part of 0.5 to be rounded either up or down seemingly randomly. So the most straightforward fix is to use `Ratio Natural` and `floor`. If the result is an integral number of picoseconds, it will give that, and for roundings, it will match the behaviour of the straightforward type-level equivalent of: type HzToPeriod (freq :: Nat) = 1_000_000_000_000 `Div` freq
|
The new (the difference being that |
gergoerdi
added a commit
to gergoerdi/retroclash-lib
that referenced
this issue
Feb 21, 2021
gergoerdi
added a commit
to gergoerdi/retroclash-lib
that referenced
this issue
Apr 21, 2021
gergoerdi
added a commit
to gergoerdi/retroclash-lib
that referenced
this issue
Jun 27, 2021
acairncross
pushed a commit
to acairncross/retroclash-lib
that referenced
this issue
Apr 6, 2023
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
One would hope that the following would be a matching type-level version of
hzToPeriod:However, because
hzToPeriodrounds up, andDivrounds down, instead we have to writeUnless there is a good reason to round up, I think it would be worth changing the implementation of
hzToPeriod(it would only change the result by 1 picosecond at most!) to be more amenable to a type-level implementation.The text was updated successfully, but these errors were encountered: