Ensuring flip flop behavior is captured by write_btor

[gussmith23]

Hi all! Thanks again for such a wonderful tool.

I use write_btor heavily. I have only recently come to discover the intricacies of the pass, though. One thing I've noticed that I'm having trouble putting words to is that write_btor sometimes doesn't capture the dependence of flip flops on their clock.

For example, if we have this module in example.v:

module example(input clk, input in, output out);
  reg r;
  always @(posedge clk) begin
    r <= in;
  end
  assign out = r;
endmodule

and we run the following command:
yosys -p "read_verilog example.v; proc; write_btor"

We get the following output:

; BTOR description generated by Yosys 0.15+50 (git sha1 6318db615, clang 10.0.0-4ubuntu1 -fPIC -Os) for module example.
1 sort bitvec 1
2 input 1 in ; example.v:1.33-1.35
3 input 1 clk ; example.v:1.22-1.25
4 state 1 r
5 output 4 out ; example.v:1.44-1.47
6 next 1 4 2
; end of yosys output

This model is correct in some sense; i.e., the input in eventually makes its way to the output out. However, it's missing a key fact: whether in makes it to out doesn't depend on clk! That is, you'd only expect the output to equal in if the clock ticked (went from 0 to 1).

It turns out we can get the btor to capture this if we use clk2fflogic:
yosys -p "read_verilog example.v; proc; clk2fflogic; write_btor"

; BTOR description generated by Yosys 0.15+50 (git sha1 6318db615, clang 10.0.0-4ubuntu1 -fPIC -Os) for module example.
1 sort bitvec 1
2 input 1 in ; example.v:1.33-1.35
3 input 1 clk ; example.v:1.22-1.25
4 state 1
5 state 1
6 const 1 1
7 state 1
8 init 1 7 6
9 sort bitvec 2
10 concat 9 3 7
11 const 9 10
12 eq 1 10 11
13 ite 1 12 5 4
14 output 13 out ; example.v:1.44-1.47
15 uext 1 13 0 r ; example.v:2.7-2.8
16 next 1 4 13
17 next 1 5 2
18 next 1 7 3
; end of yosys output

Great! This is a little more complicated, but line 12 is the key: it determines whether {clk, old_clk} == 2'b10. The output only becomes in if this is the case.

BUT: it seems like clk2fflogic is not always the right pass to use -- it breaks some of the more complex designs (specifically designs that have multiple clocks).

So here's my question. It seems like the core functionality that I'm getting from clk2fflogic is that it converts always blocks to $ff cells. However, it has other behavior that isn't as useful -- specifically, $ff cells use an implicit global clock, which ends up breaking some of my designs. What should I be using instead? I feel like I need a pass that will map always blocks to explicit-clock $dff cells (which hopefully write_btor can handle?). I thought simplemap would do it for me, but it doesn't. Can anyone help?

Update:

I'm realizing now that Yosys already sees my always blocks as $dff cells "under the hood" (i.e. in RTLIL, I think this means?) but when I run write_verilog it prints them as always blocks, and when I run write_btor, it doesn't capture the semantics of the always block as I've shown above. So why are $dff cells treated differently than $ff cells in write_btor?

[nakengelhardt]

The btor2 format doesn't have clocks, IIRC - the model just has "current state" and "next state". So there's no way to describe a multiclock design other than what clk2fflogic does, mapping everything to an implicit global clock with the different clock signals behaving sort of like enables that decide whether the state is updated in the current step or not. If you use e.g. async2sync to map to $dff and then use write_btor, it will just assume that all clock signals are identical. What is the context where you are using the btor model and what kind of "broken" is your multiclock design with it?

[gussmith23]

Thanks for the reply! I'm using the model not for verification (which I think is the intended use case) but for solver-aided synthesis (i.e. using the model of, for example, an FPGA primitive, to determine whether a design can map to that primitive). This means I need the model to very closely resemble the actual behavior of the Verilog -- so for example, if I "tick the clock" on my model, by passing 0 and then passing 1, I only want DFF outputs to be visible after the clock goes to 1. (I'm eliding a lot of details about how this works; we're working on a paper on this right now which I will be happy to share when it's done!)

Re: what kind of "broken" it is: that's a great question. All I know is that I was generating the btor from the Verilog of a large FPGA primitive, and the resulting behavior was not correct -- specifically, it seemed like the multiple clocks of the design were getting lumped together into a single clock. When I removed clk2fflogic, this stopped happening, but then the resulting models also stopped capturing the sequential behavior of the primitive: the model was fully combinational, and required zero clock ticks to get a result.

Thanks again for your reply!

[gussmith23]

Actually, I'm looking more into what was going wrong, and it seems like the problem might be that some things are getting recognized as $dffs that I actually don't want to be $dffs:

6. Executing CLK2FFLOGIC pass (convert clocked FFs to generic $ff cells).
Replacing altmult_accum.$procdff$2115 ($dff): CLK=\flag, D=\result_int, Q=\result
Replacing altmult_accum.$procdff$2116 ($dff): CLK=\flag, D=\overflow_int, Q=\overflow
Replacing altmult_accum.$procdff$2117 ($dff): CLK=\flag, D=\accum_saturate_overflow, Q=\accum_is_saturated_latent
Replacing altmult_accum.$procdff$2118 ($dff): CLK=\flag, D=\result_int, Q=\result
Replacing altmult_accum.$procdff$2119 ($dff): CLK=\flag, D=\overflow_int, Q=\overflow
Replacing altmult_accum.$procdff$2120 ($dff): CLK=\flag, D=\accum_saturate_overflow, Q=\accum_is_saturated_latent
Replacing altmult_accum.$procdff$2123 ($dff): CLK=\output_wire_clk, D=$0\result_int[4:0], Q=\result_int
Replacing altmult_accum.$procdff$2125 ($dff): CLK=\output_wire_clk, D=$0\overflow_int[0:0], Q=\overflow_int
Replacing altmult_accum.$procdff$2129 ($dff): CLK=\output_wire_clk, D=$0\accum_saturate_overflow[0:0], Q=\accum_saturate_overflow
Replacing altmult_accum.$procdff$2131 ($dff): CLK=\output_wire_clk, D=$0\accum_result[4:0], Q=\accum_result
Replacing altmult_accum.$procdff$2132 ($dff): CLK=\output_wire_clk, D=$0\mult_is_saturated_int[0:0], Q=\mult_is_saturated_int
Replacing altmult_accum.$procdff$2138 ($dff): CLK=\output_wire_clk, D=$0\flag[0:0], Q=\flag
Replacing altmult_accum.$procdff$2150 ($adff): CLK=\multiplier_wire_clk, D=$0\mult_res[3:0], Q=\mult_res
Replacing altmult_accum.$procdff$2152 ($adff): CLK=\multiplier_wire_clk, D=$0\mult_is_saturated_reg[0:0], Q=\mult_is_saturated_reg
Replacing altmult_accum.$procdff$2159 ($adff): CLK=\sign_pipe_b_wire_clk, D=$0\sign_b_pipe_reg[0:0], Q=\sign_b_pipe_reg
Replacing altmult_accum.$procdff$2160 ($adff): CLK=\sign_b_wire_clk, D=$0\sign_b_reg[0:0], Q=\sign_b_reg
Replacing altmult_accum.$procdff$2161 ($adff): CLK=\sign_pipe_a_wire_clk, D=$0\sign_a_pipe_reg[0:0], Q=\sign_a_pipe_reg
Replacing altmult_accum.$procdff$2162 ($adff): CLK=\sign_a_wire_clk, D=$0\sign_a_reg[0:0], Q=\sign_a_reg
Replacing altmult_accum.$procdff$2163 ($adff): CLK=\accum_sload_upper_data_pipe_wire_clk, D=$0\sload_upper_data_pipe_reg[0:0], Q=\sload_upper_data_pipe_reg
Replacing altmult_accum.$procdff$2164 ($adff): CLK=\zero_pipe_wire_clk, D=$0\zero_acc_pipe_reg[0:0], Q=\zero_acc_pipe_reg
Replacing altmult_accum.$procdff$2165 ($adff): CLK=\accum_sload_upper_data_wire_clk, D=$0\sload_upper_data_reg[0:0], Q=\sload_upper_data_reg
Replacing altmult_accum.$procdff$2166 ($adff): CLK=\zero_wire_clk, D=$0\zero_acc_reg[0:0], Q=\zero_acc_reg
Replacing altmult_accum.$procdff$2167 ($adff): CLK=\addsub_pipe_wire_clk, D=$0\addsub_pipe_reg[0:0], Q=\addsub_pipe_reg
Replacing altmult_accum.$procdff$2168 ($adff): CLK=\addsub_wire_clk, D=$0\addsub_reg[0:0], Q=\addsub_reg
Replacing altmult_accum.$procdff$2169 ($adff): CLK=\input_b_wire_clk, D=$0\mult_b_reg[1:0], Q=\mult_b_reg
Replacing altmult_accum.$procdff$2170 ($adff): CLK=\input_a_wire_clk, D=$0\mult_a_reg[1:0], Q=\mult_a_reg

Specifically, most of these $dffs are correct, but the top ones which have CLK=\flag are not. I don't want those to become $ffs. Is there any way to deselect those specifically?

[nakengelhardt]

I don't think it's reliably possible to reverse the transformation to $ff that clk2fflogic does to reconstitute the original clock signal, so it might not be the right approach in a synthesis context (although if you keep the pre-clk2fflogic design around, you might be able to use the conclusions of the solver on that). There's a similar issue with abc, and there what we do is to separate each clock domain and pass them individually to abc to handle. For example here they are identified in abc:

yosys/passes/techmap/abc.cc

Lines 2006 to 2167 in a9c792d

	CellTypes ct(design);
	std::vector<RTLIL::Cell*> all_cells = mod->selected_cells();
	pool<RTLIL::Cell*> unassigned_cells(all_cells.begin(), all_cells.end());
	pool<RTLIL::Cell*> expand_queue, next_expand_queue;
	pool<RTLIL::Cell*> expand_queue_up, next_expand_queue_up;
	pool<RTLIL::Cell*> expand_queue_down, next_expand_queue_down;
	typedef tuple<bool, RTLIL::SigSpec, bool, RTLIL::SigSpec, bool, RTLIL::SigSpec, bool, RTLIL::SigSpec> clkdomain_t;
	dict<clkdomain_t, std::vector<RTLIL::Cell*>> assigned_cells;
	dict<RTLIL::Cell*, clkdomain_t> assigned_cells_reverse;
	dict<RTLIL::Cell*, pool<RTLIL::SigBit>> cell_to_bit, cell_to_bit_up, cell_to_bit_down;
	dict<RTLIL::SigBit, pool<RTLIL::Cell*>> bit_to_cell, bit_to_cell_up, bit_to_cell_down;
	for (auto cell : all_cells)
	{
	clkdomain_t key;
	for (auto &conn : cell->connections())
	for (auto bit : conn.second) {
	bit = assign_map(bit);
	if (bit.wire != nullptr) {
	cell_to_bit[cell].insert(bit);
	bit_to_cell[bit].insert(cell);
	if (ct.cell_input(cell->type, conn.first)) {
	cell_to_bit_up[cell].insert(bit);
	bit_to_cell_down[bit].insert(cell);
	}
	if (ct.cell_output(cell->type, conn.first)) {
	cell_to_bit_down[cell].insert(bit);
	bit_to_cell_up[bit].insert(cell);
	}
	}
	}
	if (!RTLIL::builtin_ff_cell_types().count(cell->type))
	continue;
	FfData ff(&initvals, cell);
	if (!ff.has_clk)
	continue;
	if (ff.has_gclk)
	continue;
	if (ff.has_aload)
	continue;
	if (ff.has_sr)
	continue;
	if (!ff.is_fine)
	continue;
	key = clkdomain_t(
	ff.pol_clk,
	ff.sig_clk,
	ff.has_ce ? ff.pol_ce : true,
	ff.has_ce ? assign_map(ff.sig_ce) : RTLIL::SigSpec(),
	ff.has_arst ? ff.pol_arst : true,
	ff.has_arst ? assign_map(ff.sig_arst) : RTLIL::SigSpec(),
	ff.has_srst ? ff.pol_srst : true,
	ff.has_srst ? assign_map(ff.sig_srst) : RTLIL::SigSpec()
	);
	unassigned_cells.erase(cell);
	expand_queue.insert(cell);
	expand_queue_up.insert(cell);
	expand_queue_down.insert(cell);
	assigned_cells[key].push_back(cell);
	assigned_cells_reverse[cell] = key;
	}
	while (!expand_queue_up.empty() || !expand_queue_down.empty())
	{
	if (!expand_queue_up.empty())
	{
	RTLIL::Cell *cell = *expand_queue_up.begin();
	clkdomain_t key = assigned_cells_reverse.at(cell);
	expand_queue_up.erase(cell);
	for (auto bit : cell_to_bit_up[cell])
	for (auto c : bit_to_cell_up[bit])
	if (unassigned_cells.count(c)) {
	unassigned_cells.erase(c);
	next_expand_queue_up.insert(c);
	assigned_cells[key].push_back(c);
	assigned_cells_reverse[c] = key;
	expand_queue.insert(c);
	}
	}
	if (!expand_queue_down.empty())
	{
	RTLIL::Cell *cell = *expand_queue_down.begin();
	clkdomain_t key = assigned_cells_reverse.at(cell);
	expand_queue_down.erase(cell);
	for (auto bit : cell_to_bit_down[cell])
	for (auto c : bit_to_cell_down[bit])
	if (unassigned_cells.count(c)) {
	unassigned_cells.erase(c);
	next_expand_queue_up.insert(c);
	assigned_cells[key].push_back(c);
	assigned_cells_reverse[c] = key;
	expand_queue.insert(c);
	}
	}
	if (expand_queue_up.empty() && expand_queue_down.empty()) {
	expand_queue_up.swap(next_expand_queue_up);
	expand_queue_down.swap(next_expand_queue_down);
	}
	}
	while (!expand_queue.empty())
	{
	RTLIL::Cell *cell = *expand_queue.begin();
	clkdomain_t key = assigned_cells_reverse.at(cell);
	expand_queue.erase(cell);
	for (auto bit : cell_to_bit.at(cell)) {
	for (auto c : bit_to_cell[bit])
	if (unassigned_cells.count(c)) {
	unassigned_cells.erase(c);
	next_expand_queue.insert(c);
	assigned_cells[key].push_back(c);
	assigned_cells_reverse[c] = key;
	}
	bit_to_cell[bit].clear();
	}
	if (expand_queue.empty())
	expand_queue.swap(next_expand_queue);
	}
	clkdomain_t key(true, RTLIL::SigSpec(), true, RTLIL::SigSpec(), true, RTLIL::SigSpec(), true, RTLIL::SigSpec());
	for (auto cell : unassigned_cells) {
	assigned_cells[key].push_back(cell);
	assigned_cells_reverse[cell] = key;
	}
	log_header(design, "Summary of detected clock domains:\n");
	for (auto &it : assigned_cells)
	log(" %d cells in clk=%s%s, en=%s%s, arst=%s%s, srst=%s%s\n", GetSize(it.second),
	std::get<0>(it.first) ? "" : "!", log_signal(std::get<1>(it.first)),
	std::get<2>(it.first) ? "" : "!", log_signal(std::get<3>(it.first)),
	std::get<4>(it.first) ? "" : "!", log_signal(std::get<5>(it.first)),
	std::get<6>(it.first) ? "" : "!", log_signal(std::get<7>(it.first)));
	for (auto &it : assigned_cells) {
	clk_polarity = std::get<0>(it.first);
	clk_sig = assign_map(std::get<1>(it.first));
	en_polarity = std::get<2>(it.first);
	en_sig = assign_map(std::get<3>(it.first));
	arst_polarity = std::get<4>(it.first);
	arst_sig = assign_map(std::get<5>(it.first));
	srst_polarity = std::get<6>(it.first);
	srst_sig = assign_map(std::get<7>(it.first));
	abc_module(design, mod, script_file, exe_file, liberty_files, genlib_files, constr_file, cleanup, lut_costs, !clk_sig.empty(), "$",
	keepff, delay_target, sop_inputs, sop_products, lutin_shared, fast_mode, it.second, show_tempdir, sop_mode, abc_dress);
	assign_map.set(mod);
	}
	}

In abc9 it's a bit more complex as it also has to handle the whitebox features.

Regarding the $dff with a clock signal named flag, if you don't want that to become a $dff that must be an issue with the way the input code is written. Can you show the corresponding verilog?

[gussmith23]

I figured it out -- I actually think that the inference of flag being a clock signal was not wrong at all. In the end, I rewrote some of the Verilog to make it more amenable for the type of conversion I'm trying to do.

Thanks all for your help on this!