From: Jacob Lifshay <programmerjake@gmail.com>
Date: Fri, 10 Dec 2021 21:54:22 +0000 (-0800)
Subject: add ternlogi to shift_rot formal test
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=798afa4ccda4a0e8065e03dcf90fb60922ba4b00;p=soc.git

add ternlogi to shift_rot formal test
---

diff --git a/src/soc/fu/shift_rot/formal/proof_main_stage.py b/src/soc/fu/shift_rot/formal/proof_main_stage.py
index a515481a..7c712a46 100644
--- a/src/soc/fu/shift_rot/formal/proof_main_stage.py
+++ b/src/soc/fu/shift_rot/formal/proof_main_stage.py
@@ -55,6 +55,7 @@ class Driver(Elaboratable):
         comb += rec.insn.eq(AnyConst(rec.insn.width))
 
         pspec = ShiftRotPipeSpec(id_wid=2, parent_pspec=None)
+        pspec.draft_bitmanip = True
         m.submodules.dut = dut = ShiftRotMainStage(pspec)
 
         # convenience variables
@@ -234,6 +235,13 @@ class Driver(Elaboratable):
                 pass
             with m.Case(MicrOp.OP_RLCL):
                 pass
+            with m.Case(MicrOp.OP_TERNLOG):
+                lut = dut.fields.FormTLI.TLI[:]
+                for i in range(64):
+                    idx = Cat(dut.i.rb[i], dut.i.ra[i], dut.i.rc[i])
+                    for j in range(8):
+                        with m.If(j == idx):
+                            comb += Assert(dut.o.o.data[i] == lut[j])
             with m.Default():
                 comb += o_ok.eq(0)