`read_blif; write_blif; read_blif;` doesn't work

[navidjafarof]

Version

Final Version

On which OS did this happen?

Linux

Reproduction Steps

I am currently trying to read a blif file with Yosys, run the ABC9 pass on it, and write it as a blif file. I encountered a double definition of a signal when trying to read the blif with ABC. The same thing happens when trying to read the blif using Yosys. Yosys cannot read a blif file generated by itself. I used different blif files and got the same results. This is a and_latch module as an example.

.model and_latch
.inputs and_latch^clock and_latch^a_in and_latch^b_in
.outputs and_latch^out

.names gnd
.names unconn
.names vcc
1

.latch and_latch^bAND~0^lAND~1 and_latch^out_FF re and_latch^clock 3

.names and_latch^a_in and_latch^b_in and_latch^bAND~0^lAND~1
11 1

.names and_latch^out_FF and_latch^out
1 1

.end

Here is my terminal log for your reference

yosys> read_blif and_latch.blif 
1. Executing BLIF frontend.

yosys> write_blif output.blif

2. Executing BLIF backend.

yosys> read_blif output.blif 

3. Executing BLIF frontend.
ERROR: Duplicate definition of module and_latch in line 3!

Here are some other blif files for your reference. adder.blif.txt sv.blif.txt

Expected Behavior

The expected behavior is writing a blif file that can be read by Yosys and ABC.

Actual Behavior

The write_blif command is saving the blif file in the wrong way that cannot be re-read.

[povik]

What happens in the terminal log you provide is expected behavior. When you are running read_blif for the second time, there's an and_latch module loaded into the design already. You can run design -reset before read_blif to get a clean slate.

Having inserted design -reset before the second read I don't come across any issue with adder.blif.txt, but I get the following when trying to re-read sv.blif.txt, and a similar one when re-reading and_latch:

3. Executing BLIF frontend.
ERROR: Found error in internal cell \sv_chip0_hierarchy_no_mem.$auto$blifparse.cc:386:parse_blif$74008 ($ff) at kernel/rtlil.cc:1041:
  cell $ff $auto$blifparse.cc:386:parse_blif$74008
    connect \Q \sv_chip0_hierarchy_no_mem.ints_fifo_1_gen_1_3^dout~1_FF
    connect \D \n55328
  end

That seems to be a bug indeed, but different from what you report.

I encountered a double definition of a signal when trying to read the blif with ABC.

Trying to get ABC read the BLIF file written by Yosys for and_latch, I get

Line 10: Cannot find the model for subcircuit $dff.
Reading network from file has failed.

That seems to be some other issue. I am not familiar with BLIF files and the tooling around it to say if this is supposed to work.

Anyway, please update the reproduction steps so that it illustrates the actual issue you are running into.

[navidjafarof]

You were right about the adder.blif and and_latch.blif files. But even when exiting Yosys completely and restarting it again the following happens with the sv.blif file which was uploaded earlier.

Also, after running the ABC9 pass on the and_latch.blif file and writing it on another blif file. It cannot be read again by Yosys,

yosys> read_blif and_latch.blif 
1. Executing BLIF frontend.

yosys> abc9 -lut 6
.
.
.
yosys> write_blif and_latch2.blif

3. Executing BLIF backend.

yosys> exit

End of script. Logfile hash: d5187a3525, CPU: user 0.05s system 0.00s, MEM: 13.59 MB peak
Yosys 0.36+61 (git sha1 df65634e0, clang  14.0.0-1ubuntu1.1 -fPIC -Os)
Time spent: 60% 1x abc9_exe (0 sec), 21% 5x read_verilog (0 sec), ...

yosys> read_blif and_latch2.blif 
1. Executing BLIF frontend.
ERROR: Found error in internal cell \and_latch.$auto$blifparse.cc:386:parse_blif$1 ($dff) at kernel/rtlil.cc:1041:
  cell $dff $auto$blifparse.cc:386:parse_blif$1
    connect \Q \and_latch^out_FF
    connect \D \and_latch^bAND~0^lAND~1
    connect \CLK \and_latch^clock
  end

This is the behavior I get after running the ABC9 pass on the and_latch.blif. I appreciate it if you let me know that I am running the pass the right way.

I am getting the same error in both situations. Thank you for your time and concern.

[povik]

I looked some more into this. The issue boils down to read_blif using coarse-level flip-flop cells ($ff, $dff and similar) to represent the sequential elements from the BLIF input, but write_blif expecting fine-level flip-flop cells ($_FF_, $_DFF_P_, $_DFF_N_ etc.) when writing out the output.

I appreciate it if you let me know that I am running the pass the right way.

I would say you are, and we need to make the change for read_blif to use $_FF_ instead of $ff. ($_FF_ is different from $ff by always being single-bit.)

In the meantime, you might as a workaround use techmap t:$ff which converts $ff to $_FF_.

So e.g. the following sequence of commands does work:

read_blif sv.blif.txt
techmap t:$ff
write_blif sv.blif.txt.save
design -reset
read_blif sv.blif.txt.save

[navidjafarof]

Dear @povik, I was wondering if your pull request for this issue is ready to be merged into the Master branch. Thank you for your time.