[Libre-soc-bugs] [Bug 340] formal proof of POWER9 SHIFTROT pipeline needed

[bugzilla-daemon at libre-soc.org]

https://bugs.libre-soc.org/show_bug.cgi?id=340

Samuel A. Falvo II <kc5tja at arrl.net> changed:

           What    |Removed                     |Added
----------------------------------------------------------------------------
             Status|CONFIRMED                   |IN_PROGRESS

--- Comment #3 from Samuel A. Falvo II <kc5tja at arrl.net> ---
I cannot get the formal proofs for this pipeline working at all.  See the
following error:

```
======================================================================
ERROR: test_formal (proof_main_stage.ALUTestCase)
----------------------------------------------------------------------
Traceback (most recent call last):
  File
"/home/kc5tja/git/libre-soc/soc/src/soc/fu/shift_rot/formal/proof_main_stage.py",
line 174, in test_formal
    self.assertFormal(module, mode="bmc", depth=2)
  File "/home/kc5tja/git/libre-soc/nmutil/src/nmutil/formaltest.py", line 97,
in assertFormal
    rtlil=rtlil.convert(Fragment.get(spec, platform="formal"))
  File "/home/kc5tja/git/libre-soc/nmigen/nmigen/hdl/ir.py", line 39, in get
    obj = obj.elaborate(platform)
  File
"/home/kc5tja/git/libre-soc/soc/src/soc/fu/shift_rot/formal/proof_main_stage.py",
line 68, in elaborate
    dut_sig = getattr(dut.o.ctx.op, name)
  File "/home/kc5tja/git/libre-soc/nmigen/nmigen/hdl/rec.py", line 149, in
__getattr__
    return self[name]
  File "/home/kc5tja/git/libre-soc/nmigen/nmigen/hdl/rec.py", line 160, in
__getitem__
    raise AttributeError("{} does not have a field '{}'. Did you mean one of:
{}?"
AttributeError: Record 'alu_op' does not have a field 'alu_op__insn_type'. Did
you mean one of: insn_type, fn_unit, imm_data, rc, oe, invert_a, zero_a,
invert_out, write_cr0, input_carry, output_carry, is_32bit, is_signed,
data_len, insn?
```

I tried changing all references of AluOp to SrOp, but I get the exact same
errors.  I'm at a loss.  Can anyone provide guidance?  Thanks.

-- 
You are receiving this mail because:
You are on the CC list for the bug.