Add SMV tests for ternary, toint and floor

Author: augustomafra

tests/encoders/inputs/smv/real_arithmetic.smv

@@ -0,0 +1,15 @@
+-- SMV description generated by Yosys 0.51+101 (git sha1 6bd6775c3, g++ 11.4.0-1ubuntu1~22.04.2 -Og -fPIC)
+MODULE main
+  VAR
+    _a : real; -- a
+    _b : unsigned word[3]; -- b
+  DEFINE
+    _$itor$arithmetic#sv#7$2_Y := toint(resize(_b, 3));
+    _c := _$itor$arithmetic#sv#7$2_Y + _a;
+    _$itor$arithmetic#sv#8$5_Y := toint(resize(signed(_b), 3));
+    _$add$arithmetic#sv#8$4_Y := _a + _$itor$arithmetic#sv#8$5_Y;
+    _$eq$arithmetic#sv#8$6_Y := resize(word1(_c = _$add$arithmetic#sv#8$4_Y), 1);
+    _$auto$rtlil#cc#2837#Not$9 := !resize(_$eq$arithmetic#sv#8$6_Y, 1);
+    _$auto$rtlil#cc#2884#And$11 := resize(_$auto$rtlil#cc#2837#Not$9, 1) & resize(0ub1_1, 1);
+  INVARSPEC bool(_$eq$arithmetic#sv#8$6_Y);
+-- end of yosys output

tests/encoders/inputs/smv/real_arithmetic_floor.smv

@@ -0,0 +1,12 @@
+-- SMV description generated by Yosys 0.51+101 (git sha1 6bd6775c3, g++ 11.4.0-1ubuntu1~22.04.2 -Og -fPIC)
+MODULE main
+  VAR
+    _VIN : real; -- VIN
+    _rst1 : unsigned word[1]; -- rst1
+    _rst2 : unsigned word[1]; -- rst2
+  DEFINE
+    _delta := 1.00000000000000000 / 8.00000000000000000;
+    _$div$maurice2024_adc#sv#46$14_Y := _VIN / _delta;
+    _$floor$maurice2024_adc#sv#46$15_Y := signed word[3](floor(_$div$maurice2024_adc#sv#46$14_Y));
+  INVARSPEC bool(word1(_$floor$maurice2024_adc#sv#46$15_Y = 0sb3_000));
+-- end of yosys output

tests/encoders/inputs/smv/ternary.smv

@@ -0,0 +1,9 @@
+MODULE main
+  VAR
+    a: boolean;
+    b: boolean;
+    c: boolean;
+    d: boolean;
+  DEFINE
+    result := a ? 0.0 : b ? 1.0 : c ? 2.0 : d ? 3.0 : 4.0;
+  INVARSPEC result < 5.0;

tests/encoders/test_encoder_inputs.h

@@ -34,6 +34,9 @@ const unordered_map<string, pono::ProverResult> smv_inputs(
       { "combined-true.smv", pono::ProverResult::TRUE },
       { "counter_yosys.smv", pono::ProverResult::FALSE },
       { "counter_bitvector.smv", pono::ProverResult::FALSE },
-      { "counter_boolean.smv", pono::ProverResult::FALSE } });
+      { "counter_boolean.smv", pono::ProverResult::FALSE },
+      { "ternary.smv", pono::ProverResult::TRUE },
+      { "real_arithmetic.smv", pono::ProverResult::TRUE },
+      { "real_arithmetic_floor.smv", pono::ProverResult::FALSE } });
 
 }  // namespace pono_tests