From b4845876bda25756c2bb6fe21efcd28f502f1508 Mon Sep 17 00:00:00 2001 From: Michael Nolan Date: Fri, 8 May 2020 12:35:51 -0400 Subject: [PATCH] Convert alu to use the op in ctx --- src/soc/alu/formal/proof_input_stage.py | 21 ++++++++++++--------- src/soc/alu/input_stage.py | 5 +++-- src/soc/alu/pipe_data.py | 3 +-- 3 files changed, 16 insertions(+), 13 deletions(-) diff --git a/src/soc/alu/formal/proof_input_stage.py b/src/soc/alu/formal/proof_input_stage.py index b11ec4f3..ab679e01 100644 --- a/src/soc/alu/formal/proof_input_stage.py +++ b/src/soc/alu/formal/proof_input_stage.py @@ -23,7 +23,15 @@ class Driver(Elaboratable): m = Module() comb = m.d.comb - pspec = ALUPipeSpec(id_wid=2, op_wid=1) + rec = CompALUOpSubset() + recwidth = 0 + # Setup random inputs for dut.op + for p in rec.ports(): + width = p.width + recwidth += width + comb += p.eq(AnyConst(width)) + + pspec = ALUPipeSpec(id_wid=2, op_wid=recwidth) m.submodules.dut = dut = ALUInputStage(pspec) a = Signal(64) @@ -33,20 +41,15 @@ class Driver(Elaboratable): a.eq(AnyConst(64)), b.eq(AnyConst(64))] - # Setup random inputs for dut.op - rec = CompALUOpSubset() - for p in rec.ports(): - width = p.width - comb += p.eq(AnyConst(width)) - comb += dut.i.op.eq(rec) + comb += dut.i.ctx.op.eq(rec) # Assert that op gets copied from the input to output for p in rec.ports(): name = p.name rec_sig = p - dut_sig = getattr(dut.o.op, name) + dut_sig = getattr(dut.o.ctx.op, name) comb += Assert(dut_sig == rec_sig) with m.If(rec.invert_a): @@ -61,7 +64,7 @@ class Driver(Elaboratable): return m class GTCombinerTestCase(FHDLTestCase): - def test_gt_combiner(self): + def test_formal(self): module = Driver() self.assertFormal(module, mode="bmc", depth=4) self.assertFormal(module, mode="cover", depth=4) diff --git a/src/soc/alu/input_stage.py b/src/soc/alu/input_stage.py index ccf00301..950f5ba4 100644 --- a/src/soc/alu/input_stage.py +++ b/src/soc/alu/input_stage.py @@ -18,11 +18,10 @@ class ALUInputStage(PipeModBase): m = Module() comb = m.d.comb - comb += self.o.op.eq(self.i.op) a = Signal.like(self.i.a) - with m.If(self.i.op.invert_a): + with m.If(self.i.ctx.op.invert_a): comb += a.eq(~self.i.a) with m.Else(): comb += a.eq(self.i.a) @@ -31,4 +30,6 @@ class ALUInputStage(PipeModBase): comb += self.o.b.eq(self.i.b) + comb += self.o.ctx.eq(self.i.ctx) + return m diff --git a/src/soc/alu/pipe_data.py b/src/soc/alu/pipe_data.py index cd79abaf..a1bbc7c3 100644 --- a/src/soc/alu/pipe_data.py +++ b/src/soc/alu/pipe_data.py @@ -7,7 +7,6 @@ from ieee754.fpcommon.getop import FPPipeContext class IntegerData: def __init__(self, pspec): - self.op = CompALUOpSubset() self.ctx = FPPipeContext(pspec) self.muxid = self.ctx.muxid @@ -38,7 +37,7 @@ class IntPipeSpec: def __init__(self, id_wid=2, op_wid=1): self.id_wid = id_wid self.op_wid = op_wid - self.opkls = CompALUOpSubset + self.opkls = lambda _: CompALUOpSubset(name="op") class ALUPipeSpec(IntPipeSpec): def __init__(self, id_wid, op_wid): -- 2.30.2