Often, when performing fixed-point multiplication, it is sufficient to return a faithfully rounded result, i.e., the machine representable number either immediately above or below the arbitrary precision result, if the latter is not exactly representable. Compared to correctly rounded multipliers, i.e., those returning the nearest machine representable number, faithfully rounded multipliers use considerably less silicon area, typically by implementing a truncation scheme within the partial product array. A number of such heuristically inspired schemes exist in the literature, however their use in industrial practice is hampered by the absence of verification, and exhaustive simulation is typically infeasible, e.g., a 32 bit multiplier requires 2 64 simulations. We present three truncated multiplier schemes which subsume the majority of existing schemes and derive both closed form necessary and sufficient conditions for faithful rounding. For two of the schemes we provide closed form expressions for the bit vectors giving rise to the worst-case error and the probability of encountering these inputs during Monte-Carlo simulation. From these expressions, we show how HDL code can be created that performs correct-by-construction faithfully rounded multiplication. We also present a method for truncating an arbitrary array while maintaining faithful rounding, creating two novel truncated multiplier schemes in the process.