my $input_file = "dump.vcd";