This pull request makes the following contributions:
Refactor the conversion routines in DW1000.System_Time so that all code is in SPARK.
Replace the Long_Float calculations in DW1000.Ranging with fixed-point equivalents.
Replace the Distance fixed-point type with a Meters (single) floating-point type.
The current implementation of DW1000.System_Time hides certain conversion functions from SPARK, which is not ideal since: a) that code cannot be proved; and b) the definition of the conversion is not available to the prover to help with proofs that use the conversion routines. Therefore, they have been replaced with conversions that can be in 100% SPARK.
The implementation of the DW1000.Double_Sided and DW1000.Single_Sided packages make extensive use of Long_Float to perform the calculations. These have been replaced with fixed-point equivalents since double-width FPUs are not really available on typical microcontrollers, so must fall back to a software implementation which is slow and integer math should be faster.
Finally, the Distance fixed-point type is replaced with a single-precision floating point type to avoid issues converting between fixed-point types. See the description in commit e8f4593 for details.
This pull request makes the following contributions:
DW1000.System_Time
so that all code is in SPARK.DW1000.Ranging
with fixed-point equivalents.Distance
fixed-point type with aMeters
(single) floating-point type.The current implementation of
DW1000.System_Time
hides certain conversion functions from SPARK, which is not ideal since: a) that code cannot be proved; and b) the definition of the conversion is not available to the prover to help with proofs that use the conversion routines. Therefore, they have been replaced with conversions that can be in 100% SPARK.The implementation of the
DW1000.Double_Sided
andDW1000.Single_Sided
packages make extensive use ofLong_Float
to perform the calculations. These have been replaced with fixed-point equivalents since double-width FPUs are not really available on typical microcontrollers, so must fall back to a software implementation which is slow and integer math should be faster.Finally, the
Distance
fixed-point type is replaced with a single-precision floating point type to avoid issues converting between fixed-point types. See the description in commit e8f4593 for details.