vector-diff: vector store not diff enough times

Kconfig

@@ -276,7 +276,7 @@ config DIFFTEST_STORE_COMMIT_AMO
 config DIFFTEST_STORE_QUEUE_SIZE
   depends on DIFFTEST_STORE_COMMIT
   int "Size of committed store queue"
-  default 512
+  default 256
 
 config GUIDED_EXEC
   depends on SHARE

include/cpu/difftest.h

@@ -41,9 +41,7 @@ extern void (*ref_difftest_exec)(uint64_t n);
 extern void (*ref_difftest_raise_intr)(uint64_t NO);
 #ifdef CONFIG_DIFFTEST_STORE_COMMIT
 extern int  (*ref_difftest_store_commit)(uint64_t *addr, uint64_t *data, uint8_t *mask);
-extern void store_commit_queue_push(uint64_t addr, uint64_t data, int len);
 extern store_commit_t *store_commit_queue_pop();
-extern int check_store_commit(uint64_t *addr, uint64_t *data, uint8_t *mask);
 #endif
 static inline bool difftest_check_reg(const char *name, vaddr_t pc, rtlreg_t ref, rtlreg_t dut) {
   if (ref != dut) {
@@ -64,16 +62,18 @@ static inline bool difftest_check_vreg(const char *name, vaddr_t pc, rtlreg_t *r
 }
 #ifdef CONFIG_DIFFTEST_STORE_COMMIT
 static inline bool difftest_check_store(vaddr_t pc) {
-  store_commit_t *dut =  store_commit_queue_pop();
-  if (dut == NULL) return true;
-  uint64_t dut_data = dut->data;
-  uint64_t dut_addr = dut->addr;
-
-  if (ref_difftest_store_commit(&dut->addr, &dut->data, &dut->mask)) {
-    Log("\n\t,is different memory executing instruction at pc = " FMT_WORD,pc);
-    Log(",ref addr = " FMT_WORD ", data = " FMT_WORD "\n\t dut addr = " FMT_WORD ", data = " FMT_WORD 
-        ,dut->addr, dut->data, dut_addr, dut_data);  
-    return false;
+  uint64_t step = store_read_step();
+  for (int i = 0; i < step ;i ++) {
+    store_commit_t *dut =  store_commit_queue_pop();
+    if (dut == NULL) return true;
+    uint64_t dut_data = dut->data;
+    uint64_t dut_addr = dut->addr;
+    if (ref_difftest_store_commit(&dut->addr, &dut->data, &dut->mask)) {
+      Log("\n\t,is different memory executing instruction at pc = " FMT_WORD,pc);
+      Log(",ref addr = " FMT_WORD ", data = " FMT_WORD "\n\t dut addr = " FMT_WORD ", data = " FMT_WORD ", step = "FMT_WORD
+          ,dut->addr, dut->data, dut_addr, dut_data, step);  
+      return false;
+    }
   }
   return true;
 }

include/memory/paddr.h

@@ -77,6 +77,7 @@ extern store_commit_t store_commit_queue[CONFIG_DIFFTEST_STORE_QUEUE_SIZE];
 void store_commit_queue_push(uint64_t addr, uint64_t data, int len);
 store_commit_t *store_commit_queue_pop();
 int check_store_commit(uint64_t *addr, uint64_t *data, uint8_t *mask);
+uint64_t store_read_step();
 #endif
 
 #ifdef CONFIG_MULTICORE_DIFF

src/memory/paddr.c

@@ -83,6 +83,7 @@ static inline word_t pmem_read(paddr_t addr, int len) {
   #ifdef CONFIG_USE_SPARSEMM
   return sparse_mem_wread(sparse_mm, addr, len);
   #else
+  Logm("pmpm read %lx, len %d", addr, len);
   return host_read(guest_to_host(addr), len);
   #endif
 }
@@ -91,7 +92,7 @@ static inline void pmem_write(paddr_t addr, int len, word_t data) {
 #ifdef CONFIG_DIFFTEST_STORE_COMMIT
   store_commit_queue_push(addr, data, len);
 #endif
-
+  Logm("pmpm write %lx, len %d, data %lx", addr, len, data);
   #ifdef CONFIG_USE_SPARSEMM
   sparse_mem_wwrite(sparse_mm, addr, len, data);
   #else
@@ -167,6 +168,8 @@ word_t paddr_read(paddr_t addr, int len, int type, int mode, vaddr_t vaddr) {
   else {
     if (likely(is_in_mmio(addr))) return mmio_read(addr, len);
     else raise_read_access_fault(type, vaddr);
+    Log("read_access_fault");
+    raise_access_fault(EX_LAF, vaddr);
     return 0;
   }
 #else
@@ -264,7 +267,7 @@ void paddr_write(paddr_t addr, int len, word_t data, int mode, vaddr_t vaddr) {
     else {
       if(dynamic_config.ignore_illegal_mem_access)
         return;
-      printf("ERROR: invalid mem write to paddr " FMT_PADDR ", NEMU raise access exception\n", addr);
+      Log("ERROR: invalid mem write to paddr " FMT_PADDR ", NEMU raise access exception\n", addr);
       raise_access_fault(EX_SAF, vaddr);
       return;
     }
@@ -343,6 +346,12 @@ int check_store_commit(uint64_t *addr, uint64_t *data, uint8_t *mask) {
   return result;
 }
 
+inline uint64_t store_read_step() {
+  if (tail >= head) 
+    return tail - head;
+  else 
+    return (CONFIG_DIFFTEST_STORE_QUEUE_SIZE - head + tail);
+}
 #endif
 
 char *mem_dump_file = NULL;