pymtl / pymtl3

Pymtl 3 (Mamba), an open-source Python-based hardware generation, simulation, and verification framework
BSD 3-Clause "New" or "Revised" License
388 stars 46 forks source link

Incorrect range elaboration #257

Closed KelvinChung2000 closed 1 year ago

KelvinChung2000 commented 1 year ago

The following script:

import pymtl3 as pymtl
from pymtl3.passes.backends.verilog import *

class a(pymtl.Component):
    def construct(s):
        s.inTag = pymtl.InPort(pymtl.Bits8)
        s.out = pymtl.OutPort(pymtl.Bits8)
        numEntries = 4
        s.table = [pymtl.Wire(8) for _ in range(numEntries)]

        @pymtl.update_ff
        def testFail():
            for i in range(2, numEntries, 1):
                s.table[i] <<= s.inTag if s.table[i] != s.inTag else s.table[i]

        # @pymtl.update_ff
        # def testPass():
        #     s.table[2] <<= s.inTag if s.table[2] != s.inTag else s.table[2]
        #     s.table[3] <<= s.inTag if s.table[3] != s.inTag else s.table[3]

        @pymtl.update_ff
        def test():
            s.table[0] <<= s.inTag if s.table[0] != s.inTag else s.table[0]
            s.table[1] <<= s.inTag if s.table[1] != s.inTag else s.table[1]

if __name__ == "__main__":
    m = a()
    m.elaborate()
    m.apply(pymtl.DefaultPassGroup())
    m.inTag @= 10
    print(m.table)
    m.sim_tick()
    print(m.table)

When running with the testFail block, it will give the following error:

pymtl3.dsl.errors.MultiWriterError: Multiple update blocks write s.table[1].
 - test at s
 - testFail at s

the range function should set i to should 2 and 3, so, s.table[1] should not getting written at testFail.

cbatten commented 1 year ago

I don't think our elaboration analysis pass is sophisticated enough to understand what you are doing here ... it cannot figure out that the testFail update block writes a disjoint set of the entires in the table compared to the test update block ... It would actually be pretty difficult to figure this out .. our elaboration pass would need to understand the semantics of the for loop (and possibly nested for loops, conditionals, etc) to prove that the writes from different update blocks to the same array of signals are always writing disjoint elements in that array ...

Is there any reason you cannot do the writes in the same update block? that should probably work?

  @pymtl.update_ff
  def testFail():
    for i in range(2, numEntries, 1):
      s.table[i] <<= s.inTag if s.table[i] != s.inTag else s.table[i]
    s.table[0] <<= s.inTag if s.table[0] != s.inTag else s.table[0]
    s.table[1] <<= s.inTag if s.table[1] != s.inTag else s.table[1]
KelvinChung2000 commented 1 year ago

I can write them in a single block. I am just doing some testing and running into this by accident.

cbatten commented 1 year ago

OK! My suggestion is to keep all writes to an array of signals in a single update block ... thanks for posting!