Synthesis error for D-latch

[danilovesky]

Complex gate, gC, and stdC synthesis failed for D-latch, with several errors in the log and a segfault in the end.

Here is dlatch.lpn:

# LPN file generated by Workcraft 3 (Return of the Hazard), version 3.2.0
.name D_latch
#@.init_state [000]
.inputs C D
.outputs Q
.graph
C+/0 C1
C+/1 C1
C-/0 C+/0 D1Q1
C-/1 C+/1 D0Q0
D+/0 Q+/0
D-/0 Q-/0
Q+/0 C1 D1Q1
Q-/0 C1 D0Q0
C1 C-/0 C-/1 Q+/0 Q-/0
D0Q0 C-/1 D+/0
D1Q1 C-/0 D-/0
.marking {<C-/1,C+/1> D0Q0}
.end

The log and the produced auxiliary files are in dlatch.zip

The expected Verilog output is something like:

module Q_C_D_net(Q, C, D);
    output Q;
    input C, D;

    assign Q = C & D | ~C & Q;

    // Initial state:
    // !C !D !Q
endmodule

[cjmyers]

I don't see a seg fault, but this example is not legal. The output Q is disabled. Here is the log I get:

ATACS VERSION 6.0 Logging session in: atacs.log PARG output on errors disabled. Using single-cube algorithm for synthesis. Initial state vector has 3 entries, but there are 0 IOs. Converting Petri net to ER and storing to: dlatch.er Loading timed event-rule structure from: dlatch.er WARNING: Duplicate rules ignored. Initializing 3 cycles ... done Checking for cycles in acyclic constraint graph ... ERROR! ERROR: Cycle detected in acyclic constraint graph. Finding reduced state graph ... ERROR! ERROR: Output event Q+/0 is disabled Finding the trace! Error found after exploring 10 states Storing error trace state graph to: dlatch.dino Storing full error trace state graph to: dlatch.trace D+/0 -> C+/1 -> Q+/0 -> D-/0 -> Q-/0 -> D+/0 -> C-/1 -> FAIL!

This error trace looks legal to me, please check. Do other tools synthesize? The error also feels correct to me, since you cannot build a speed-independent dlatch. Namely, what if clock changes before Q changes, which is precisely the error found.

BTW: I don't get a seg fault. Could you try with the "-oq" at the beginning of your command line. This is quiet mode which will prevent it from trying to open the error trace in parg and/or dinotrace. This may be what is causing your seg faults.

[danilovesky]

@cjmyers Thanks for pointing to -oq option, it did help. Most likely the segfault was caused by setup (absence of some tools). With -oq option it is much better, at least on this D-latch example.

Regarding the trace -- I do not see how after D+/0 -> C+/1 -> Q+/0 -> D-/0 -> Q-/0 -> D+/0 transition C-/1 gets enabled. In my simulation it does not... If it was enabled then its firing would disable Q+/0 indeed. Can this be the cause of the issue?

Here is a simulation screenshot after trace D+/0 -> C+/1 -> Q+/0 -> D-/0 -> Q-/0 -> D+/0 . At this state only Q+/0 is enabled, but not C-/1:

And yes, both Petrify and MPSat manage to synthesise D-latch as Q = C & D | ~C & Q.

[cjmyers]

So the problem is that ATACS originally did not use Petri-nets, but instead it used a graph called a Timed Event/Rule Structure. It is similar but conflict is quite different. The conflict in this graph is complicated, so the conversion from LPN to TERS is not working correctly. However, ATACS now does support Petri-nets, so you can use the LPN loader instead. To do this, add "-ll" before "-ys" which says to load the file using the LPN loader. When I add this switch, I get:

/*

• dlatch */ module C_D_Q_net(C, D, Q);

  input C; input D; output Q;

assign Q = (C & D) | (~C | D) & Q;

// Initial state: // !C !D !Q

endmodule

NOTE: I'm not sure if this will change any of your other results, so you may want to double check all the other benchmarks.

[danilovesky]

Thanks @cjmyers , this -ll option did the trick for D-latch (and few other examples)! All "old" benchmark also produce the same result as before, so no regression.