amaranth-lang / amaranth

A modern hardware definition language and toolchain based on Python
https://amaranth-lang.org/docs/amaranth/
BSD 2-Clause "Simplified" License
1.55k stars 170 forks source link

Detect and reject netlists with combinatorial loops #704

Closed sporniket closed 5 months ago

sporniket commented 2 years ago

Originally posted by @whitequark in https://github.com/amaranth-lang/amaranth/issues/703#issuecomment-1104789392

In general, if the simulator doesn't converge, it means an issue with the input netlist. I'd say that the appropriate way to handle this is to reject such netlists before they can be simulated, since by the time the simulator is stuck, the original issue (a logic loop of some kind) becomes very hard to find.

⇒ Questions

whitequark commented 2 years ago

This is not an RFC: no design is presented that can be commented on.

Also, this issue is not exclusive to the simulator: designs with combinatorial feedback loops are unsound and may be silently miscompiled during synthesis as well.

widlarizer commented 1 year ago

As far as I can tell, this requires the following, done on the entire design, or on fragments with combinational domains guaranteed to be disconnected:

for every combinational assignment s.eq(e):
    for every signal s' in expression e:
        add edge (s', s)

We get an oriented graph. If all is good, it is a forest. If there's a comb loop, there's a cycle. So we look for it with DFS from all states, most of these terminating immediately. I don't know where this traversal should happen. I have looked at xfrm.py, we could use some sort of Visitor. Maybe it should be implemented in the elaborate method of Module? Or at the highest level in cli.py before conversion or sim?

widlarizer commented 1 year ago

I'm building a prototype using Visitors from xfrm.py and have determined that the prepare method in ir.py. Not sure how to get "fully qualified" signal names or IDs yet.

whitequark commented 1 year ago

I think this isn't something I'm considering integrating in the next few development cycles, sorry.

widlarizer commented 1 year ago

Understood. Is the project structure likely to change until it may become relevant? I'm still probably going to get it done, it's fine by me if it stays in my fork for half a year or forever, I'm doing it for rather academic reasons

widlarizer commented 1 year ago

I have a functional prototype at fd673627c94ddb38357bb0cead5ddd03628e2920. Next step: testing if it works across ports, reporting what loop was found, if Switch dependencies work as intended, and measuring slowdown on large projects caused by this. I believe it's all nice and linear with signals and assignments and Value tree sizes, but we'll see

whitequark commented 1 year ago

Is the project structure likely to change until it may become relevant?

Yes, the current system of Fragment rewriting is likely going away entirely.

whitequark commented 7 months ago

The new IR now makes this possible. We'll need a cell edges database though. @wanda-phi