initial
assume (= [mem_0] [mem_1])
assume (= [cpu_0.cpuregs] [cpu_1.cpuregs])
assume (= [trace_data_0] [trace_data_1])

always
assume (=> (not [mem_valid_0]) (not [mem_ready_0]))
assume (=> (not [mem_valid_1]) (not [mem_ready_1]))
# assume (= [mem_ready_0] [mem_ready_1])

always -1
assert (=> (= [trace_balance] #x00) (= [trace_data_0] [trace_data_1]))