A co-worker who couldn't get his login to work asked me to post this for him:
Try specifying the clock attributes with ‘netlist clock’. For example,
netlist clock clk1 clk2 clk3 –posedge –period 4 –waveform 0 2
By default, formal analysis uses the existing netlist clock directives
to determine $global_clock, which is the union of the active clock
edges. So the behavior you want should be the default when you
do not specify clocks. However, if you have registers clocked on
negedges, I am not sure whether or not this will work.