m-labs / nmigen

A refreshed Python toolbox for building complex digital hardware. See https://gitlab.com/nmigen/nmigen
https://nmigen.org
Other
652 stars 55 forks source link

Initial Class: ValueError: call stack is not deep enough #318

Closed goktug97 closed 4 years ago

goktug97 commented 4 years ago

I am trying to use Initial() like https://github.com/m-labs/nmigen/blob/57d95b7f95dd37e2527db7b04be9ac8f324133e2/nmigen/test/test_lib_fifo.py#L213-L217 this. I run test_lib_fifo.py to make sure it works.

from nmigen.test import test_lib_fifo
a = test_lib_fifo.FIFOFormalCase()
a.test_sync_fwft_npot()

It didn't throw any error but my version throws this error.

Traceback (most recent call last):
  File "counter.py", line 20, in <module>
    with m.If(Initial()):
  File "/home/goktug/.local/lib/python3.8/site-packages/nmigen/hdl/ast.py", line 1184, in __init__
    super().__init__(src_loc_at=1 + src_loc_at)
  File "/home/goktug/.local/lib/python3.8/site-packages/nmigen/hdl/ast.py", line 129, in __init__
    self.src_loc = tracer.get_src_loc(1 + src_loc_at)
  File "/home/goktug/.local/lib/python3.8/site-packages/nmigen/tracer.py", line 54, in get_src_loc
    frame = sys._getframe(2 + src_loc_at)
ValueError: call stack is not deep enough

I am using nmigen to formal verify verilog and VHDL files. https://github.com/m-labs/nmigen/issues/317

from nmigen import *
from nmigen.cli import main_parser, main_runner
from nmigen.build import *
from nmigen.back import *
from nmigen.asserts import Assert, Cover, Past, Assume, Rose, Initial, Stable

if __name__ == '__main__':
    parser = main_parser()
    args = parser.parse_args()

    clk = ClockSignal()
    reset = ResetSignal()
    enable = Signal()
    count = Signal(4)
    counter = Instance('counter',
                       i_clk=clk, i_reset=reset, i_enable=enable, o_count=count)

    m = Module()
    m.submodules.counter = counter

    with m.If(Initial()):
        m.d.sync += Assert(1)

    m.d.sync += Assume(count < 0b1111)
    with m.If(Rose(clk)):
        with m.If(Past(enable) & ~reset & ~Past(reset)):
            m.d.sync += Assert((Past(count) + 1) == count)
        with m.Elif(reset):
            m.d.sync += Assert(count == 0)

    main_runner(parser, args, m, ports=[clk, reset, enable, count])
whitequark commented 4 years ago

Fixed in nmigen/nmigen@a14a572.

goktug97 commented 4 years ago

The stack error is gone. Unfortunately, I got this error when I try to use sby with generated verilog file,

SBY 18:59:45 [counter] base: ERROR: Module `\$initstate' referenced in module `\top' in cell `\U$$0' is not part of the design.
whitequark commented 4 years ago

@goktug97 You should use the RTLIL backend with SymbiYosys rather than the Verilog one.

goktug97 commented 4 years ago

Using RTLIL backend solves the problem.