From 555d1e4397f9e750b186f4c07ef3172b7ee39c0d Mon Sep 17 00:00:00 2001
From: Albert Magyar
Date: Wed, 12 Feb 2020 22:21:44 -0800
Subject: Add Ops equiv check to stress degenerate binary op ConstProp

* Send in the Yosys
---
 .travis.yml     |  6 ++++++
 regress/Ops.fir | 54 ++++++++++++++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 60 insertions(+)
 create mode 100644 regress/Ops.fir

diff --git a/.travis.yml b/.travis.yml
index d1d6cd64..2065cb56 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -76,6 +76,12 @@ jobs:
         - yosys -V
         - "travis_wait 30 sleep 1800 &"
         - ./.run_formal_checks.sh ICache
+    - stage: test
+      name: "Formal equivalence: Ops"
+      script:
+        - yosys -V
+        - "travis_wait 30 sleep 1800 &"
+        - ./.run_formal_checks.sh Ops
     - stage: test
       script:
         - benchmark/scripts/benchmark_cold_compile.py -N 2 --designs regress/ICache.fir --versions HEAD
diff --git a/regress/Ops.fir b/regress/Ops.fir
new file mode 100644
index 00000000..51cffad5
--- /dev/null
+++ b/regress/Ops.fir
@@ -0,0 +1,54 @@
+circuit Ops:
+  module Ops:
+    input sel: UInt<4>
+    input is: SInt<8>
+    input iu: UInt<8>
+    output os: SInt<14>
+    output ou: UInt<13>
+    output obool: UInt<1>
+
+    os <= SInt(0)
+    ou <= UInt(0)
+    obool <= UInt(0)
+
+    when eq(sel, UInt(0)):
+      os <= add(is, is)
+      ou <= add(iu, iu)
+    else:
+      when eq(sel, UInt(1)):
+        os <= sub(is, is)
+        ou <= sub(iu, iu)
+      else:
+        when eq(sel, UInt(2)):
+          os <= mux(eq(is, SInt(0)), SInt(1), div(is, is))
+          ou <= mux(eq(iu, UInt(0)), UInt(1), div(iu, iu))
+        else:
+          when eq(sel, UInt(3)):
+            os <= rem(is, is)
+            ou <= rem(iu, iu)
+          else:
+            when eq(sel, UInt(4)):
+              ou <= add(and(is, is), and(iu, iu))
+            else:
+              when eq(sel, UInt(5)):
+                ou <= add(or(is, is), or(iu, iu))
+              else:
+                when eq(sel, UInt(4)):
+                  ou <= add(xor(is, is), xor(iu, iu))
+                else:
+                  when eq(sel, UInt(5)):
+                    ou <= add(eq(is, is), eq(iu, iu))                
+                  else:
+                    when eq(sel, UInt(4)):
+                      ou <= add(neq(is, is), neq(iu, iu))
+                    else:
+                      when eq(sel, UInt(5)):
+                        ou <= add(geq(is, is), geq(iu, iu))
+                      else:
+                        when eq(sel, UInt(4)):
+                          ou <= add(leq(is, is), leq(iu, iu))
+                        else:
+                          when eq(sel, UInt(5)):
+                            ou <= add(gt(is, is), gt(iu, iu))
+                          else:
+                            ou <= add(lt(is, is), lt(iu, iu))
-- 
cgit v1.2.3