log("Dumping SAT model to WaveJSON file '%s'.\n", json_file_name.c_str());
 
-               std::string module_fname = "unknown";
-               auto apos = module->attributes.find("\\src");
-               if(apos != module->attributes.end())
-                       module_fname = module->attributes["\\src"].decode_string();
-
-               fprintf(f, "// Generated by %s\n", yosys_version_str);
-
                int mintime = 1, maxtime = 0, maxwidth = 0;;
                dict<string, pair<int, dict<int, Const>>> wavedata;
 
                        maxwidth = std::max(maxwidth, info.width);
                }
 
-               fprintf(f, "{ signal: [\n");
-               for (auto &wd : wavedata) {
+               fprintf(f, "{ \"signal\": [");
+               bool fist_wavedata = true;
+               for (auto &wd : wavedata)
+               {
+                       fprintf(f, "%s", fist_wavedata ? "\n" : ",\n");
+                       fist_wavedata = false;
+
                        vector<string> data;
                        string name = wd.first.c_str();
                        while (name.substr(0, 1) == "\\")
                                name = name.substr(1);
-                       fprintf(f, "    { name: '%s', wave: '", name.c_str());
+
+                       fprintf(f, "    { \"name\": \"%s\", \"wave\": \"", name.c_str());
                        for (int i = mintime; i <= maxtime; i++) {
                                if (wd.second.second.count(i)) {
                                        string this_data = wd.second.second[i].as_string();
                                }
                        }
                        if (wd.second.first != 1) {
-                               fprintf(f, "', data: [");
+                               fprintf(f, "\", \"data\": [");
                                for (int i = 0; i < GetSize(data); i++)
-                                        fprintf(f, "%s'%s'", i ? ", " : "", data[i].c_str());
-                               fprintf(f, "] },\n");
+                                        fprintf(f, "%s\"%s\"", i ? ", " : "", data[i].c_str());
+                               fprintf(f, "] }");
                        } else {
-                               fprintf(f, "' },\n");
+                               fprintf(f, "\" }");
                        }
                }
-               fprintf(f, "  ],\n");
-               fprintf(f, "  config: {\n");
-               fprintf(f, "    hscale: %.2f,\n", maxwidth / 4.0);
-               fprintf(f, "  },\n");
+               fprintf(f, "\n  ],\n");
+               fprintf(f, "  \"config\": {\n");
+               fprintf(f, "    \"hscale\": %.2f\n", maxwidth / 4.0);
+               fprintf(f, "  }\n");
                fprintf(f, "}\n");
                fclose(f);
        }