diff options
| -rw-r--r-- | .travis.yml | 6 | ||||
| -rw-r--r-- | regress/Ops.fir | 54 |
2 files changed, 60 insertions, 0 deletions
diff --git a/.travis.yml b/.travis.yml index d1d6cd64..2065cb56 100644 --- a/.travis.yml +++ b/.travis.yml @@ -77,5 +77,11 @@ jobs: - "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)) |