Whitespace

[soc.git] / src / soc / fu / compunits / formal / proof_fu.py

diff --git a/src/soc/fu/compunits/formal/proof_fu.py b/src/soc/fu/compunits/formal/proof_fu.py
index 56c75b7ba3f3bf57b02038f85a6e42a6e14b8fa7..0af6ea6437ea501ff4441f0bd2c08361d5110997 100644 (file)
--- a/src/soc/fu/compunits/formal/proof_fu.py
+++ b/src/soc/fu/compunits/formal/proof_fu.py
@@ -9,13 +9,15 @@ from nmigen import (Module, Signal, Elaboratable, Mux, Cat, Repl,
 from nmigen.asserts import (Assert, AnyConst, Assume, Cover, Initial,
                             Rose, Fell, Stable, Past)
 from nmutil.formaltest import FHDLTestCase
+from nmutil.gtkw import write_gtkw
 from nmigen.cli import rtlil
 import unittest
+import os
 
 from soc.fu.compunits.compunits import FunctionUnitBaseSingle
 from soc.experiment.alu_hier import DummyALU
 from soc.experiment.compalu_multi import MultiCompUnit
-from soc.fu.alu.alu_input_record import CompALUOpSubset
+from soc.fu.cr.cr_input_record import CompCROpSubset
 
 
 class Driver(Elaboratable):
@@ -26,17 +28,23 @@ class Driver(Elaboratable):
         m = Module()
         comb = m.d.comb
         sync = m.d.sync
+        inspec = [('INT', 'a', '0:15'),
+                  ('INT', 'b', '0:15'),
+                  ('INT', 'c', '0:15')]
+        outspec = [('INT', 'o', '0:15')]
+
+        regspec = (inspec, outspec)
         alu = DummyALU(16)
-        m.submodules.dut = dut = MultiCompUnit(16, alu, CompALUOpSubset)
+        m.submodules.dut = dut = MultiCompUnit(regspec, alu, CompCROpSubset)
 
         issue = dut.issue_i
         busy = dut.busy_o
 
-        go_rd = dut.rd.go
-        rd_rel = dut.rd.rel
+        go_rd = dut.rd.go_i
+        rd_rel = dut.rd.rel_o
 
-        go_wr = dut.wr.go
-        wr_rel = dut.wr.rel
+        go_wr = dut.wr.go_i
+        wr_rel = dut.wr.rel_o
 
         go_die = dut.go_die_i
         shadow_n = dut.shadown_i
@@ -52,6 +60,7 @@ class Driver(Elaboratable):
             comb += Assume(issue == 0)
             comb += Assume(go_rd == 0)
             comb += Assume(rst == 1)
+
         with m.Else():
             comb += Assume(rst == 0)
 
@@ -71,7 +80,6 @@ class Driver(Elaboratable):
             # cycle. Read requests may go out immediately after issue
             # goes low
 
-
             # The read_request should not happen while the unit is not busy
             with m.If(~busy):
                 comb += Assert(rd_rel == 0)
@@ -131,7 +139,6 @@ class Driver(Elaboratable):
             with m.If(wr_rel == 0):
                 comb += Assume(go_wr == 0)
 
-
             # Property 8: When go_write is asserted, two things
             # happen. 1 - the data in the temp register is placed
             # combinatorially onto the output. And 2 - the req_l latch
@@ -142,14 +149,14 @@ class Driver(Elaboratable):
             # then the alu data should be output
             with m.If(Past(wr_rel) & Past(go_wr)):
                 # the alu data is output
-                comb += Assert((dut.data_o == alu_temp) | (dut.data_o == dut.alu.o))
+                comb += Assert((dut.data_o == alu_temp)
+                               | (dut.data_o == dut.alu.o))
                 # wr_rel is dropped
                 comb += Assert(wr_rel == 0)
                 # busy is dropped.
                 with m.If(~Past(go_die)):
                     comb += Assert(busy == 0)
 
-
         # It is REQUIRED that issue be held valid only for one cycle
         with m.If(Past(issue)):
             comb += Assume(issue == 0)
@@ -182,11 +189,57 @@ class Driver(Elaboratable):
 
 class FUTestCase(FHDLTestCase):
     def test_formal(self):
+        style = {
+            'in': {'color': 'orange'},
+            'out': {'color': 'yellow'},
+        }
+        traces = [
+            'clk',
+            ('operation port', {'color': 'red'}, [
+                'cu_issue_i', 'cu_busy_o',
+                {'comment': 'shadow / go_die'},
+                'cu_shadown_i', 'cu_go_die_i']),
+            ('operand 1 port', 'in', [
+                ('cu_rd__rel_o[2:0]', {'bit': 2}),
+                ('cu_rd__go_i[2:0]', {'bit': 2}),
+                'src1_i[15:0]']),
+            ('operand 2 port', 'in', [
+                ('cu_rd__rel_o[2:0]', {'bit': 1}),
+                ('cu_rd__go_i[2:0]', {'bit': 1}),
+                'src2_i[15:0]']),
+            ('operand 3 port', 'in', [
+                ('cu_rd__rel_o[2:0]', {'bit': 0}),
+                ('cu_rd__go_i[2:0]', {'bit': 0}),
+                'src1_i[15:0]']),
+            ('result port', 'out', [
+                'cu_wr__rel_o', 'cu_wr__go_i', 'dest1_o[15:0]']),
+            ('alu', {'submodule': 'alu'}, [
+                ('prev port', 'in', [
+                    'oper_i_None__insn_type', 'i1[15:0]',
+                    'valid_i', 'ready_o']),
+                ('next port', 'out', [
+                    'alu_o[15:0]', 'valid_o', 'ready_i'])])]
+
+        write_gtkw('test_fu_formal_bmc.gtkw',
+                   os.path.dirname(__file__) +
+                   '/proof_fu_formal/engine_0/trace.vcd',
+                   traces, style,
+                   clk_period=10e-9,
+                   time_resolution_unit="ns",
+                   module='top.dut')
+
         module = Driver()
         self.assertFormal(module, mode="bmc", depth=10)
         self.assertFormal(module, mode="cover", depth=10)
+
     def test_ilang(self):
-        dut = MultiCompUnit(16, DummyALU(16), CompALUOpSubset)
+        inspec = [('INT', 'a', '0:15'),
+                  ('INT', 'b', '0:15'),
+                  ('INT', 'c', '0:15')]
+        outspec = [('INT', 'o', '0:15')]
+
+        regspec = (inspec, outspec)
+        dut = MultiCompUnit(regspec, DummyALU(16), CompCROpSubset)
         vl = rtlil.convert(dut, ports=dut.ports())
         with open("multicompunit.il", "w") as f:
             f.write(vl)