Three engines to solve verification constraints of decimal Floating-Point operation

Decimal floating-point designs require a verification process to prove that the design is in compliance with the IEEE Standard for Floating-Point Arithmetic (IEEE Std 754-2008). Our work represents three engines, the first engine for the verification of decimal addition-subtraction operation, the second for the verification of decimal multiplication operation, and the third for the verification of decimal fused-multiple-add operation. Each engine solves constraints describing all corner cases of the operation, and generates test vectors to verify these corner cases in the tested design. The paper describes the constraints of each operation and the steps of each engine to solve these constraints.