Allow the formal engine to perform a same-cycle result in the ALU

[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 bba929004c0b4e453430a3d28e39c87a3d4e9f00..9ec497fa7060a41fe21c6429a3235ab1fb035792 100644 (file)
--- a/src/soc/fu/compunits/formal/proof_fu.py
+++ b/src/soc/fu/compunits/formal/proof_fu.py
@@ -9,8 +9,10 @@ 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 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
 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.fu.compunits.compunits import FunctionUnitBaseSingle
 from soc.experiment.alu_hier import DummyALU


@@ -58,6 +60,7 @@ class Driver(Elaboratable):
             comb += Assume(issue == 0)
             comb += Assume(go_rd == 0)
             comb += Assume(rst == 1)
             comb += Assume(issue == 0)
             comb += Assume(go_rd == 0)
             comb += Assume(rst == 1)

+

         with m.Else():
             comb += Assume(rst == 0)
 
         with m.Else():
             comb += Assume(rst == 0)
 


@@ -77,7 +80,6 @@ class Driver(Elaboratable):
             # cycle. Read requests may go out immediately after issue
             # goes low
 
             # 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)
             # The read_request should not happen while the unit is not busy
             with m.If(~busy):
                 comb += Assert(rd_rel == 0)


@@ -112,12 +114,12 @@ class Driver(Elaboratable):
             alu_temp = Signal(16)
             write_req_valid = Signal(reset=0)
             with m.If(~Past(go_die) & Past(busy)):
             alu_temp = Signal(16)
             write_req_valid = Signal(reset=0)
             with m.If(~Past(go_die) & Past(busy)):

-                with m.If(Rose(dut.alu.n.valid_o)):
+                with m.If(Rose(dut.alu.n.o_valid)):

                     sync += alu_temp.eq(dut.alu.o)
                     sync += write_req_valid.eq(1)
 
             # write_req_valid should only be high once the alu finishes
                     sync += alu_temp.eq(dut.alu.o)
                     sync += write_req_valid.eq(1)
 
             # write_req_valid should only be high once the alu finishes

-            with m.If(~write_req_valid & ~dut.alu.n.valid_o):
+            with m.If(~write_req_valid & ~dut.alu.n.o_valid):

                 comb += Assert(wr_rel == 0)
 
             # Property 6: Write request release is held up if shadow_n
                 comb += Assert(wr_rel == 0)
 
             # Property 6: Write request release is held up if shadow_n


@@ -137,7 +139,6 @@ class Driver(Elaboratable):
             with m.If(wr_rel == 0):
                 comb += Assume(go_wr == 0)
 
             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
             # 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


@@ -148,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
             # 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.o_data == alu_temp)
+                               | (dut.o_data == 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)
 
                 # 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)
         # It is REQUIRED that issue be held valid only for one cycle
         with m.If(Past(issue)):
             comb += Assume(issue == 0)


@@ -188,9 +189,49 @@ class Driver(Elaboratable):
 
 class FUTestCase(FHDLTestCase):
     def test_formal(self):
 
 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]',
+                    'i_valid', 'o_ready']),
+                ('next port', 'out', [
+                    'alu_o[15:0]', 'o_valid', 'i_ready'])])]
+
+        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)
         module = Driver()
         self.assertFormal(module, mode="bmc", depth=10)
         self.assertFormal(module, mode="cover", depth=10)

+

     def test_ilang(self):
         inspec = [('INT', 'a', '0:15'),
                   ('INT', 'b', '0:15'),
     def test_ilang(self):
         inspec = [('INT', 'a', '0:15'),
                   ('INT', 'b', '0:15'),