compile_ultra no_autoungroup
this is because dc uses many high level synthesis which makes LEC very difficult. one way is to let DC write out svf file and use formality. but we still found there is abort.
have you use compile_ultra? if so, try to use these options like
compile_ultra -no_autoungroup -no_boundary_optimization -no_seq_output_inversion -exact_map
you can noticed that DC has turn on many optimization as default.
if QoR has not much difference and you care about LEC, just use compile, most of the time, comformal LEC can pass with analyze datapath, but if the constraints is too tight, some datapath logic still failed to pass.