more init and next, file comments

tools/rotor.c

@@ -56,6 +56,7 @@ uint64_t* new_array(uint64_t* size_sid, uint64_t* element_sid, char* comment);
 uint64_t* new_constant(uint64_t constant, uint64_t* sid);
 uint64_t* new_state(uint64_t* sid, char* symbol, char* comment);
 uint64_t* new_init(uint64_t* sid, uint64_t* state_nid, uint64_t* value_nid, char* symbol, char* comment);
+uint64_t* new_next(uint64_t* sid, uint64_t* state_nid, uint64_t* value_nid, char* comment);
 
 void print_comment(uint64_t* line);
 void print_line(uint64_t nid, uint64_t* line);
@@ -64,6 +65,7 @@ void print_sort(uint64_t* line);
 void print_constant(uint64_t* line);
 void print_state(uint64_t* line);
 void print_init(uint64_t* line);
+void print_next(uint64_t* line);
 
 // ------------------------ GLOBAL CONSTANTS -----------------------
 
@@ -77,6 +79,7 @@ char* OP_SORT  = (char*) 0;
 char* OP_CONST = (char*) 0;
 char* OP_STATE = (char*) 0;
 char* OP_INIT  = (char*) 0;
+char* OP_NEXT  = (char*) 0;
 
 uint64_t* SID_BOOLEAN = (uint64_t*) 0;
 uint64_t* NID_FALSE   = (uint64_t*) 0;
@@ -114,6 +117,7 @@ void init_architecture() {
   OP_CONST = "constd";
   OP_STATE = "state";
   OP_INIT  = "init";
+  OP_NEXT  = "next";
 
   SID_BOOLEAN = new_bitvec(1, "Boolean");
   NID_FALSE   = new_constant(0, SID_BOOLEAN);
@@ -274,6 +278,10 @@ uint64_t* new_init(uint64_t* sid, uint64_t* state_nid, uint64_t* value_nid, char
   return new_line(OP_INIT, sid, state_nid, value_nid, (uint64_t*) symbol, comment);
 }
 
+uint64_t* new_next(uint64_t* sid, uint64_t* state_nid, uint64_t* value_nid, char* comment) {
+  return new_line(OP_NEXT, sid, state_nid, value_nid, UNUSED, comment);
+}
+
 void print_comment(uint64_t* line) {
   if (get_comment(line) != NOCOMMENT)
     w = w + dprintf(output_fd, " ; %s", get_comment(line));
@@ -291,6 +299,8 @@ void print_line(uint64_t nid, uint64_t* line) {
     print_state(line);
   else if (get_op(line) == OP_INIT)
     print_init(line);
+  else if (get_op(line) == OP_NEXT)
+    print_next(line);
   print_comment(line);
 }
 
@@ -321,12 +331,19 @@ void print_init(uint64_t* line) {
     OP_INIT, get_nid(get_sid(line)), get_nid(get_arg1(line)), get_nid(get_arg2(line)), (char*) get_arg3(line));
 }
 
+void print_next(uint64_t* line) {
+  w = w + dprintf(output_fd, " %s %lu %lu %lu",
+    OP_NEXT, get_nid(get_sid(line)), get_nid(get_arg1(line)), get_nid(get_arg2(line)));
+}
+
 // -----------------------------------------------------------------
 // --------------------------- REGISTERS ---------------------------
 // -----------------------------------------------------------------
 
 void new_register_file_state() {
   state_register_file = new_state(SID_REGISTER_STATE, "regs", "register file");
+  init_register_file  = new_init(SID_REGISTER_STATE, state_register_file, NID_MACHINE_WORD_0, "regs", "initial value");
+  next_register_file  = new_next(SID_REGISTER_STATE, state_register_file, state_register_file, "TBD");
 }
 
 // -----------------------------------------------------------------
@@ -335,6 +352,8 @@ void new_register_file_state() {
 
 void new_main_memory_state() {
   state_main_memory = new_state(SID_MEMORY_STATE, "mem", "main memory");
+  init_main_memory  = new_init(SID_MEMORY_STATE, state_main_memory, NID_MACHINE_WORD_0, "mem", "initial value");
+  next_main_memory  = new_next(SID_MEMORY_STATE, state_main_memory, state_main_memory, "TBD");
 }
 
 // -----------------------------------------------------------------
@@ -348,9 +367,11 @@ void new_main_memory_state() {
 void new_core_state() {
   state_core_pc = new_state(SID_MACHINE_WORD, "pc", "program counter");
   init_core_pc  = new_init(SID_MACHINE_WORD, state_core_pc, NID_MACHINE_WORD_0, "pc", "initial value");
+  next_core_pc  = new_next(SID_MACHINE_WORD, state_core_pc, state_core_pc, "TBD");
 
   state_core_ir = new_state(SID_SINGLE_WORD, "ir", "instruction register");
   init_core_ir  = new_init(SID_SINGLE_WORD, state_core_ir, NID_SINGLE_WORD_0, "ir", "initial value");
+  next_core_ir  = new_next(SID_SINGLE_WORD, state_core_ir, state_core_ir, "TBD");
 }
 
 // -----------------------------------------------------------------
@@ -364,6 +385,10 @@ void rotor() {
 
   // output RISC-U machine model
 
+  w = w
+    + dprintf(output_fd, "; %s\n\n", SELFIE_URL)
+    + dprintf(output_fd, "; BTOR2 file %s generated by %s\n\n", model_name, selfie_name);
+
   print_line(1, SID_BOOLEAN);
   print_line(2, SID_BYTE);
   print_line(3, SID_SINGLE_WORD);
@@ -376,22 +401,38 @@ void rotor() {
   print_line(7, SID_MEMORY_ADDRESS);
   print_line(8, SID_MEMORY_STATE);
 
+  w = w + dprintf(output_fd, "\n; machine constants\n\n");
+
   print_line(10, NID_FALSE);
   print_line(11, NID_TRUE);
 
   print_line(30, NID_SINGLE_WORD_0);
   if (IS64BITTARGET)
     print_line(40, NID_DOUBLE_WORD_0);
 
+  w = w + dprintf(output_fd, "\n; register file\n\n");
+
   print_line(200, state_register_file);
+  print_line(201, init_register_file);
+  print_line(202, next_register_file);
+
+  w = w + dprintf(output_fd, "\n; program counter\n\n");
 
   print_line(300, state_core_pc);
   print_line(301, init_core_pc);
+  print_line(302, next_core_pc);
+
+  w = w + dprintf(output_fd, "\n; instruction register\n\n");
 
   print_line(400, state_core_ir);
   print_line(401, init_core_ir);
+  print_line(402, next_core_ir);
+
+  w = w + dprintf(output_fd, "\n; main memory\n\n");
 
   print_line(1000, state_main_memory);
+  print_line(1001, init_main_memory);
+  print_line(1002, next_main_memory);
 }
 
 uint64_t selfie_model() {
@@ -414,6 +455,9 @@ uint64_t selfie_model() {
 
       init_architecture();
 
+      output_name = model_name;
+      output_fd   = model_fd;
+
       rotor();
 
       output_name = (char*) 0;