Update formal VexRiscv to halt on missaligned dbus

README.md

@@ -226,10 +226,9 @@ You can find some FPGA project which instantiate the Briey SoC there (DE1-SoC, D
 There is some measurements of Briey SoC timings and area : 
 
 ```
-  Artix 7    -> 256 Mhz 3302 LUT 3524 FF
+  Artix 7    -> 231 Mhz 3339 LUT 3533 FF
-  Cyclone V  -> 126 Mhz 2,295 ALMs
+  Cyclone V  -> 124 Mhz 2,264 ALMs
-  Cyclone IV -> 121 Mhz 4,781 LUT 3,713 FF
+  Cyclone IV -> 124 Mhz 4,709 LUT 3,716 FF
-  Cyclone II -> 104 Mhz 4,902 LUT 3,718 FF
 ```
 
 ## Murax SoC
@@ -280,17 +279,15 @@ There is some measurements of Murax SoC timings and area  :
 
 ```
 Murax interlocked stages (0.37 DMIPS/Mhz) ->
-  Artix 7    -> 306 Mhz 1021 LUT 1291 FF
+  Artix 7    -> 304 Mhz 1016 LUT 1296 FF
-  Cyclone V  -> 173 Mhz 752 ALMs
+  Cyclone V  -> 165 Mhz 736 ALMs
-  Cyclone IV -> 140 Mhz 1483 LUT 1,250 FF
+  Cyclone IV -> 151 Mhz 1,463 LUT 1,254 FF
-  Cyclone II -> 127 Mhz 1484 LUT 1,249 FF
   ICE40-HX   ->  51 Mhz 2387 LC (icestorm)
 
 MuraxFast bypassed stages (0.55 DMIPS/Mhz) ->
-  Artix 7    -> 310 Mhz 1192 LUT 1388 FF
+  Artix 7    -> 301 Mhz 1248 LUT 1393 FF
-  Cyclone V  -> 160 Mhz 893 ALMs
+  Cyclone V  -> 163 Mhz 872 ALMs
-  Cyclone IV -> 142 Mhz 1726 LUT 1,284 FF
+  Cyclone IV -> 145 Mhz 1,712 LUT 1,288 FF
-  Cyclone II -> 106 Mhz 1714 LUT 1,283 FF
   ICE40-HX   ->  45 Mhz, 2718 LC  (icestorm)
 ```
 

src/main/scala/vexriscv/demo/FormalSimple.scala

@@ -22,7 +22,7 @@ object FormalSimple extends App{
           catchAccessFault = false
         ),
         new DBusSimplePlugin(
-          catchAddressMisaligned = false,
+          catchAddressMisaligned = true,
           catchAccessFault = false
         ),
         new DecoderSimplePlugin(

src/main/scala/vexriscv/demo/SynthesisBench.scala

@@ -121,4 +121,13 @@ object MuraxSynthesisBench {
 
     Bench(rtls, targets, "/eda/tmp/")
   }
+}
+
+object AllSynthesisBench {
+  def main(args: Array[String]): Unit = {
+    VexRiscvSynthesisBench.main(args)
+    BrieySynthesisBench.main(args)
+    MuraxSynthesisBench.main(args)
+
+  }
 }

src/main/scala/vexriscv/plugin/DBusSimplePlugin.scala

@@ -220,8 +220,8 @@ class DBusSimplePlugin(catchAddressMisaligned : Boolean, catchAccessFault : Bool
         U(0) -> B"0001",
         U(1) -> B"0011",
         default -> B"1111"
-      )
+      ) |<< dBus.cmd.address(1 downto 0)
-      insert(FORMAL_MEM_ADDR) := dBus.cmd.address
+      insert(FORMAL_MEM_ADDR) := dBus.cmd.address & U"xFFFFFFFC"
       insert(FORMAL_MEM_WMASK) := (dBus.cmd.valid &&  dBus.cmd.wr) ? formalMask | B"0000"
       insert(FORMAL_MEM_RMASK) := (dBus.cmd.valid && !dBus.cmd.wr) ? formalMask | B"0000"
       insert(FORMAL_MEM_WDATA) := dBus.cmd.payload.data
@@ -288,7 +288,7 @@ class DBusSimplePlugin(catchAddressMisaligned : Boolean, catchAccessFault : Bool
         assert(!(arbitration.isValid && input(MEMORY_ENABLE) && !input(INSTRUCTION)(5) && arbitration.isStuck),"DBusSimplePlugin doesn't allow memory stage stall when read happend")
 
       //formal
-      insert(FORMAL_MEM_RDATA) := rspFormated
+      insert(FORMAL_MEM_RDATA) := input(MEMORY_READ_DATA)
     }
   }
 }

src/main/scala/vexriscv/plugin/FomalPlugin.scala

@@ -99,7 +99,7 @@ class FomalPlugin extends Plugin[VexRiscv]{
       rvfi.rs2.addr := output(RS2_USE) ? output(INSTRUCTION)(rs2Range).asUInt | U(0)
       rvfi.rs1.rdata := output(RS1_USE) ? output(RS1) | B(0)
       rvfi.rs2.rdata := output(RS2_USE) ? output(RS2) | B(0)
-      rvfi.rd.addr := output(REGFILE_WRITE_VALID) ? output(INSTRUCTION)(rdRange).asUInt | U(0)
+      rvfi.rd.addr := output(REGFILE_WRITE_VALID) ? (output(INSTRUCTION)(rdRange).asUInt) | U(0)
       rvfi.rd.wdata := output(REGFILE_WRITE_VALID) ? output(REGFILE_WRITE_DATA) | B(0)
       rvfi.pc.rdata := output(PC)
       rvfi.pc.wdata := output(FORMAL_PC_NEXT)