Trouble synthesising a circuit

[porridgewithraisins]

Is it possible to synthesise this and write it to aiger ?
If not, how do I change it so it is possible for this tool to synthesise it?
Is there some cell library I should include?

I tried doing

read_verilog md5.txt
synth -flatten
abc -g AND
write_aiger -ascii out.aag

which had worked when I tried to convert a different verilog design to aiger before.

If I try it on this, I get an error on the write_aiger step from the AIGER backend
ERROR: Unsupported cell type: $_DFF_PN1_ ($auto$ff.cc:262:slice$3574)

I am new to all of this, especially this tool, so excuse any ignorance.
Thanks!

[jix]

In this case, the verilog design uses async resets, which are not representable in the AIGER file format. You can use the async2sync and dffunmap passes to convert everything into plain AIGER compatible FFs, (equivalent assuming all input signals are synchronized to the clock). The complete flow would be:

read_verilog md5.txt
synth -flatten
async2sync
dffunmap
abc -g AND
write_aiger -ascii out.aag

See help async2sync and help dffunmap for more details.