1) Alloc-outbound

Has 2 mono hazards on output busctl. Both of these hazards are caused by input nodes. I can make both of these go away by changing INV delay from [1,3] to [1,2] and this makes sense to me. Also, these viol’s are gone in the .allnodes file as well. Still makes sense. However, both mono violations come back in both my verifier and Chris’s verifier when using the covered netlists. I’m not sure why. Also, there is nothing I can do to fix these mono hazards short of changing timing since the input nodes can’t be affected by covering. Or can they? Does the new timing after covering make these mono viol’s go away?

OK, I solved the covered mystery. The covered netlist viol’s come back because the inverters in the covered netlist have delays taken from the library and not the global inverter delay constant. So once I changed the library delays for an INV to [1,2] the mono violations went away. Allnodes (32,2.87), allnodes_cov(18,0.61)

2) ebergen

has 5 ack hazards on output x for decomp and my verifier. Chris’s verifier has an extra disabling on the output x. We probably miss it because of ack hazard behavior on the inputs to the CEL. After covering, my verifier has 3 hazards (nodes 16,20,21) as expected, but Chris’s verifier has 3 hazards on (16,20, and output x). All ack hazards. I don’t understand, yet. I tightened the timings in the .g file to match the covered netlists but had no effect. (see file ebergen.g.cov). I’m guessing that my verifier misses the hazard on the output because of hazard behavior at the inputs to the CEL (nodes 16,21) and that the hazard on 20 is a false negative. Allnodes (25, 1.16), allnodes_cov (17,0.36).

3) mp_forward_pkt

1 mono hazard on output alloc-outbound. The mono hazard is caused by an input node. All 3 methods catch the same hazard whether or not the allnodes covered netlist is used as compared to the allnodes uncovered netlist. A couple min time violations are reported for the covered netlist but don’t seem to make a difference. Allnodes (31, 7.89), allnodes_cov (17, 0.41)

4) Nowick

1 mono hazard on input node q for output y. It seems most of the mono hazards are caused by the input that goes into a nand2 un-inverted where the other input is inverted. All these mono hazards occur because the timing on the non-inverted input is [3,x] and the race comes because the timing on the inverter is [1,3]. Changing the inverter to [1,2] clears up this mono problem in all cases so far. Allnodes (41, 33.09), allnodes_cov (21, 0.90). The allnodes verification match for both, but mine has an extra mono violation for the allnodes_cov netlist. Changing the .g file to tighten up the timings for the covered file had no effect. These two mono violations are the same as the previous files ie. Changing inv delays would fix it. So we are seeing here another false negative.

5) Ram-read-sbuf

2 mono hazards on output wsen. Allnodes (39, 3.47), allnodes_cov (24, 0.64) Verification matches for allnodes netlist. For allnodes_cov, mine has another false negative on covered node xx13.

6) sbuf-send-ctl

For output idlebar, 2 ack hazards on nodes xx3, xx4. 1 mono hazard on node xx1. allnodes (29, 2.98), allnodes_cov (16, 0.76). My verifier for the allnodes file has one false negative compared to Chris’s verifier. The covered verification reports no hazards for both verifiers!!

7) chu133

no hazards. Allnodes (20, 0.38), allnodes_cov (10, 0.15)

8) converta

no hazards. Allnodes (46, 5.69), allnodes_cov (22, 0.51)

9) half

no hazards. Allnodes (11, 0.15), allnodes_cov (7, 0.17)

10) rcv-setup

no hazards. Allnodes (16, 0.51), allnodes_cov (7, 0.22)

11) rpdft

no hazards. Allnodes (29, 1.37), allnodes_cov (9, 0.27)

12) sbuf-send-pkt2

no hazards. Allnodes (42, 22.56), allnodes_cov (19, 1.02)

13) trimos-send

Just general comments here. The decomp.finds a number of ack and mono hazards on outputs a, b, and c and none on t1, t2, and t3 in 78 seconds. Interesting that the mono hazards are all reported on primary input nodes. My verifier on the covered netlist finishes 27 nodes in 51 seconds and has 6 hazardous nodes left but fixes all mono hazards. Chris’s verifier keeps running and reports virtually all nodes disabled before I finally stopped it.

14) sbuf-ram-write

15) sbuf read-ctl

Notes: Full verification on a covered netlist is much, much faster than the allnodes netlist.

These mono violations are occurring when the input is an output from another part of the circuit. One way to fix would be to use a special small inverter with delay of [1,2] for simply inverting the input. Another way is to not use the absolute min times through the circuit.