Simple tricks to remove topological loops when writing to BTOR?

[gussmith23]

Hi all!

I've been using the write_btor feature of Yosys heavily. Thank you for that, it's immensely useful!

One problem I run into is that a design can't be converted to BTOR when there are topological loops. I'm still unclear on exactly when these occur, and I'm unsure how to get rid of them (or if it's possible). So I have a few questions:

1. What exactly is a topological loop? I understand what it is in general, but perhaps not in the context of a Verilog design.
2. Are there easy tricks to remove topological loops? I currently do a few modifications to the design before writing to BTOR (proc; prep; flatten; clk2fflogic), but if there were other passes that would magically remove these loops, that would be wonderful. If not, is there some manual way to remove topological loops? Or does it just depend on the design?

Thanks again for Yosys, it rocks!

[nakengelhardt]

Not sure if this is what you are encountering, but there is a known issue for code where some bits of a signal depend on other bits of the same signal, such as in this example:

module top(input clk, input a, input b, output [9:0] x);
	wire [9:0] ripple;
	reg [9:0] prev_ripple = 9'b0;

	always @(posedge clk) prev_ripple <= ripple;

	assign ripple = {ripple[8:0], a} ^ prev_ripple; // only cyclic at the coarse-grain level
	assign x = ripple[9] + b;
endmodule

Because the design is elaborated at coarse-grain level, it operates on signals as a whole rather than as individual bits, and so the statement ripple = {ripple[8:0], a} ^ prev_ripple; is considered a logic loop as ripple depends on itself.

You can use the command scc -select; simplemap; select -clear to break the coarse-grain cell (here a $xor) into bitwise gates ($_XOR_). (This is already done automatically by sby, if that's what you're using - if you're having problems with loops in sby, they're probably genuine combinatorial loops.)

[gussmith23]

Thanks for the quick reply. Hopefully this works in some of the cases I'm encountering -- it doesn't work in the current case I'm looking at, though, so I assume I'm seeing a "genuine combinatorial loop" as you describe it. Will it just be impossible to make a BTOR expression, if that's the case? Or should I be trying to modify the design somehow to eliminate the combinatorial loop?

[gussmith23]

Still confused on exactly where this is coming from (despite Yosys's helpful output!), but I found that making a reset signal synchronous and not asynchronous actually "fixed" the issue. Of course, modifying the functionality of the design is not ideal, but it's at least a step forward.

[nakengelhardt]

Is the case small enough that you can share the code? If it has a loop, there isn't really any way out of that except modifying the design.