smt: run DeadCodeElimination after PropagatePresetAnnotations

[ekiwi]

This enables an important pattern in Chisel:

val preset = WireInit(false.B.asAsyncReset())
annotate(new ChiselAnnotation {
  override def toFirrtl = PresetAnnotation(preset.toTarget)
})
withReset(preset) {
  // ...
}

Note that the problematic part is the use of WireInit which is required in order not to run afoul of wire initialization checks in the compiler frontend.

Contributor Checklist

• Did you add Scaladoc to every public function/method?
• Did you update the FIRRTL spec to include every new feature/behavior?
• Did you add at least one test demonstrating the PR?
• Did you delete any extraneous printlns/debugging code?
• Did you specify the type of improvement?
• Did you state the API impact?
• Did you specify the code generation impact?
• Did you request a desired merge strategy?

Type of Improvement

• bug fix

API Impact

• none

Backend Code Generation Impact

• only affects SMT/Btor2 backends, no change to Verilog generaion

Desired Merge Strategy

• squash

Reviewer Checklist (only modified by reviewer)

• Did you add the appropriate labels?
• Did you mark the proper milestone (1.2.x, 1.3.0, 1.4.0) ?
• Did you review?
• Did you check whether all relevant Contributor checkboxes have been checked?
• Did you mark as Please Merge?

[seldridge]

Looks good. I can't comment on the interactions in smt specifically, but I trust you here.

This may hint that PropagatePresetAnnotations is invalidating DeadCodeElimination.

[ekiwi]

This may hint that PropagatePresetAnnotations is invalidating DeadCodeElimination.

I could have also fixed this by only lazily throwing errors. Essentially my problem is that there is a left over AsyncReset expression which I cannot translate. It is never used, so it is not actually a problem for the final translation. However tracking which signals are used would make my translation code harder to write.

[jackkoenig]

Looks good, just need to migrate off Travis due to extremely limited open-source credits