From: Michael Nolan <mtnolan2640@gmail.com>
Date: Wed, 11 Mar 2020 13:21:35 +0000 (-0400)
Subject: Add test for remaining bits
X-Git-Tag: div_pipeline~1720
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=25795971d57cafa33d555fb29738a3edb4ea04ce;p=soc.git

Add test for remaining bits
---

diff --git a/src/soc/decoder/formal/proof_decoder2.py b/src/soc/decoder/formal/proof_decoder2.py
index 311cf01f..30ae65db 100644
--- a/src/soc/decoder/formal/proof_decoder2.py
+++ b/src/soc/decoder/formal/proof_decoder2.py
@@ -32,6 +32,7 @@ class Driver(Elaboratable):
         self.test_in3()
         self.test_out()
         self.test_rc()
+        self.test_single_bits()
 
         return self.m
 
@@ -154,8 +155,29 @@ class Driver(Elaboratable):
             comb += Assert(pdecode2.e.rc.data == 1)
         with m.If(sel == RC.RC):
             comb += Assert(pdecode2.e.rc.data == dec.Rc[0:-1])
+            comb += Assert(pdecode2.e.oe.ok == 1)
+            comb += Assert(pdecode2.e.oe.data == dec.OE[0:-1])
+
+    def test_single_bits(self):
+        m = self.m
+        comb = self.comb
+        pdecode2 = m.submodules.pdecode2
+        dec = pdecode2.dec
+        e = pdecode2.e
+        comb += Assert(e.invert_a == dec.op.inv_a)
+        comb += Assert(e.invert_out == dec.op.inv_out)
+        comb += Assert(e.input_carry == dec.op.cry_in)
+        comb += Assert(e.output_carry == dec.op.cry_out)
+        comb += Assert(e.is_32bit == dec.op.is_32b)
+        comb += Assert(e.is_signed == dec.op.sgn)
+        with m.If(dec.op.lk):
+            comb += Assert(e.lk == dec.LK[0:-1])
+        comb += Assert(e.byte_reverse == dec.op.br)
+        comb += Assert(e.sign_extend == dec.op.sgn_ext)
+        comb += Assert(e.update == dec.op.upd)
+        comb += Assert(e.input_cr == dec.op.cr_in)
+        comb += Assert(e.output_cr == dec.op.cr_out)
 
-        
 
 class Decoder2TestCase(FHDLTestCase):
     def test_decoder2(self):