Fix case where exception exit and entry are requested simultaneously. Fix interaction between exception exit and pipe stall/flush.

Author: Wren6991

TODO.todo

@@ -10,14 +10,18 @@ Processor:
   ☐ Compliant debug support (must run with upstream openocd)
   ☐ Support for M extension
     ✔ Create divide/multiply circuit @done (20-02-26 00:00)
-    ☐ Integrate into pipeline, pass compliance tests
-    ☐ Kill ongoing div/mul on IRQ raise
+    ✔ Integrate into pipeline, pass compliance tests @done (20-02-28 21:05)
+    ✔ Kill ongoing div/mul on IRQ raise @done (20-03-02 00:45)
     ☐ Fuse MULH/MUL and DIV/REM sequences
+    ✔ Get riscv-formal M-extension checks passing with ALTOPS enabled @done (20-03-02 00:44)
+    ☐ Get all riscv-formal rv32imc checks passing with muldiv instantiated
+    ☐ Standalone formal test for mul/div results
   ☐ Support two-bus-master variant
     ☐ Write separate top levels for 1mst and 2mst
     ☐ Bring up compliance tests on 2mst
     ☐ Bring up riscv-formal on 2mst
     ☐ Yosys synth check for through-paths between the two busmasters
+  ☐ Bring up riscv-formal CSR checks
   ☐ Integrate riscv-formal into regressions, perhaps optionally.
   ☐ Iterate on decode synths to try and pack gates down
     Still an open issue. Have investigated the instruction decompressor and it's no larger than the crazy hand-Espresso'd one in SWeRV. Rest of decode potentially still has some savings in the non-RV-specific parts.

hdl/hazard5/hazard5_cpu.v

@@ -353,8 +353,8 @@ reg  [W_MEMOP-1:0]   xm_memop;
 // For JALR, the LSB of the result must be cleared by hardware
 wire [W_ADDR-1:0] x_taken_jump_target = dx_jump_is_regoffs ? x_alu_add & ~32'h1 : dx_jump_target;
 wire [W_ADDR-1:0] x_jump_target =
+	x_trap_exit                                 ? x_mepc             : // Note precedence -- it's possible to have enter && exit, but in this case enter_rdy is false.
 	x_trap_enter                                ? x_trap_addr        :
-	x_trap_exit                                 ? x_mepc             :
 	dx_imm[31] && dx_branchcond != BCOND_ALWAYS ? dx_mispredict_addr :
 	                                              x_taken_jump_target;
 
@@ -401,7 +401,7 @@ always @ (*) begin
 		MEMOP_SH:  ahb_hsize_d = HSIZE_HWORD;
 		default:   ahb_hsize_d = HSIZE_BYTE;
 	endcase
-	ahb_req_d = x_memop_vld && !x_stall_raw && !flush_d_x && !x_trap_enter;
+	ahb_req_d = x_memop_vld && !(x_stall_raw || flush_d_x || x_trap_enter);
 end
 
 // ALU operand muxes and bypass
@@ -441,11 +441,17 @@ end
 wire   x_except_ecall         = dx_except == EXCEPT_ECALL;
 wire   x_except_breakpoint    = dx_except == EXCEPT_EBREAK;
 wire   x_except_invalid_instr = dx_except == EXCEPT_INSTR_ILLEGAL;
-wire   x_trap_enter_rdy       = !(x_stall || m_jump_req);
-assign x_trap_exit            = dx_except == EXCEPT_MRET && x_trap_enter_rdy;
+assign x_trap_exit            = dx_except == EXCEPT_MRET && !(x_stall || m_jump_req);
+wire   x_trap_enter_rdy       = !(x_stall || m_jump_req || x_trap_exit);
+wire   x_trap_is_exception; // diagnostic
 
 `ifdef FORMAL
-always @ (posedge clk) if (flush_d_x) assert(!x_trap_enter_rdy);
+always @ (posedge clk) begin
+	if (flush_d_x)
+		assert(!x_trap_enter_rdy);
+	if (x_trap_exit)
+		assert(!ahb_req_d);
+end
 `endif
 
 wire [W_DATA-1:0] x_csr_wdata = dx_csr_w_imm ?
@@ -479,6 +485,7 @@ hazard5_csr #(
 	.trap_enter_vld          (x_trap_enter),
 	.trap_enter_rdy          (x_trap_enter_rdy),
 	.trap_exit               (x_trap_exit),
+	.trap_is_exception       (x_trap_is_exception),
 	.mepc_in                 (dx_pc),
 	.mepc_out                (x_mepc),
 	// IRQ and exception requests

hdl/hazard5/hazard5_csr.v

@@ -70,6 +70,7 @@ module hazard5_csr #(
 	output wire            trap_enter_vld,
 	input  wire            trap_enter_rdy,
 	input  wire            trap_exit,
+	output wire            trap_is_exception, // diagnostic
 	output wire [XLEN-1:0] mepc_in,
 	output wire [XLEN-1:0] mepc_out,
 
@@ -742,8 +743,27 @@ wire [11:0] mtvec_offs = (exception_req_any ?
 
 assign trap_addr = mtvec | mtvec_offs;
 assign trap_enter_vld = CSR_M_TRAP && (exception_req_any || irq_any);
+assign trap_is_exception = exception_req_any;
 
 assign mcause_irq_next = !exception_req_any;
 assign mcause_code_next = exception_req_any ? exception_req_num : irq_num;
 
+// ----------------------------------------------------------------------------
+
+`ifdef RISCV_FORMAL
+always @ (posedge clk) begin
+	// Something is screwed up if this happens
+	if ($past(trap_enter_vld && trap_enter_rdy))
+		assert(!wen);
+	// Don't do this
+	assert(!(trap_enter_vld && trap_enter_rdy && trap_exit));
+	// Should be impossible to get into the trap and exit it so quickly:
+	if (in_trap && !$past(in_trap))
+		assert(!trap_exit);
+	// Should be impossible to get to another mret so soon after exiting:
+	assert(!(trap_exit && $past(trap_exit)));
+end
+
+`endif
+
 endmodule