From 7b8da0a13b13c4ef3b6c7cf1b31a39d29a4c0475 Mon Sep 17 00:00:00 2001 From: stuartjh Date: Thu, 13 Aug 2020 16:33:35 -0400 Subject: [PATCH] cleaning up repo --- core/branch_predictor.sv | 39 ++- core/branch_predictor_ram.sv | 1 + core/csr_regs.sv | 6 +- core/dcache.sv | 60 +++- core/div_unit.sv | 12 +- core/dtag_banks.sv | 22 +- core/external_interfaces.sv | 11 + core/fetch.sv | 31 +- core/gc_unit.sv | 17 +- core/icache.sv | 7 +- .../instruction_metadata_and_id_management.sv | 8 +- core/load_store_unit.sv | 78 ++++- core/shift_counter.sv | 2 +- core/taiga.sv | 325 ++++++++++++++++-- core/tlb_lut_ram.sv | 7 +- formal/scripts/setup_taiga_dev.tcl | 4 +- l2_arbiter/l2_external_interfaces.sv | 14 + l2_arbiter/l2_interfaces.sv | 1 + local_memory/local_memory_interface.sv | 1 + 19 files changed, 561 insertions(+), 85 deletions(-) diff --git a/core/branch_predictor.sv b/core/branch_predictor.sv index 62da954..8116299 100755 --- a/core/branch_predictor.sv +++ b/core/branch_predictor.sv @@ -84,18 +84,31 @@ module branch_predictor ( generate if (USE_BRANCH_PREDICTOR) for (i=0; i 1) - one_hot_to_integer #(BRANCH_PREDICTOR_WAYS) hit_way_conv (.*, .one_hot(tag_matches), .int_out(hit_way)); + one_hot_to_integer #(BRANCH_PREDICTOR_WAYS) hit_way_conv ( + .clk (clk), + .rst (rst), + .one_hot(tag_matches), + .int_out(hit_way) + ); else assign hit_way = 0; endgenerate @@ -155,7 +173,12 @@ module branch_predictor ( //////////////////////////////////////////////////// //Instruction Fetch metadata - cycler #(BRANCH_PREDICTOR_WAYS) replacement_policy (.*, .en(1'b1), .one_hot(replacement_way)); + cycler #(BRANCH_PREDICTOR_WAYS) replacement_policy ( + .clk (clk), + .rst (rst), + .en (1'b1), + .one_hot (replacement_way) + ); assign branch_metadata_if.branch_predictor_metadata = if_entry[hit_way].metadata; assign branch_metadata_if.branch_prediction_used = use_predicted_pc; diff --git a/core/branch_predictor_ram.sv b/core/branch_predictor_ram.sv index 863e985..6d2eb2b 100644 --- a/core/branch_predictor_ram.sv +++ b/core/branch_predictor_ram.sv @@ -30,6 +30,7 @@ module branch_predictor_ram ) ( input logic clk, + input logic rst, input logic [$clog2(C_DEPTH)-1:0] write_addr, input logic write_en, input logic [$clog2(C_DEPTH)-1:0] read_addr, diff --git a/core/csr_regs.sv b/core/csr_regs.sv index 4559131..1055a22 100755 --- a/core/csr_regs.sv +++ b/core/csr_regs.sv @@ -70,6 +70,10 @@ module csr_regs (* ramstyle = "MLAB, no_rw_check" *) logic[XLEN-1:0] scratch_regs [31:0];//Only 0x1 and 0x3 used by supervisor and machine mode respectively logic[XLEN-1:0] scratch_out; + + privilege_t privilege_level; + privilege_t next_privilege_level; + mip_t sip_mask; mie_t sie_mask; logic[XLEN-1:0] sepc; @@ -164,8 +168,6 @@ module csr_regs //////////////////////////////////////////////////// //Non-Constant Registers mstatus_t mstatus; - privilege_t privilege_level; - privilege_t next_privilege_level; logic[XLEN-1:0] mtvec; logic[XLEN-1:0] medeleg; diff --git a/core/dcache.sv b/core/dcache.sv index 61e0109..114b238 100755 --- a/core/dcache.sv +++ b/core/dcache.sv @@ -30,9 +30,9 @@ module dcache( input logic dcache_on, l1_arbiter_request_interface.master l1_request, l1_arbiter_return_interface.master l1_response, - input sc_complete, - input sc_success, - input clear_reservation, + input logic sc_complete, + input logic sc_success, + input logic clear_reservation, input data_access_shared_inputs_t ls_inputs, output logic[31:0] data_out, @@ -171,11 +171,26 @@ module dcache( //////////////////////////////////////////////////// //Replacement policy (free runing one-hot cycler, i.e. pseudo random) - cycler #(DCACHE_WAYS) replacement_policy (.*, .en(1'b1), .one_hot(replacement_way)); + cycler #(DCACHE_WAYS) replacement_policy ( + .clk (clk), + .rst (rst), + .en (1'b1), + .one_hot (replacement_way) + ); //One-hot tag hit / update logic to binary int - one_hot_to_integer #(DCACHE_WAYS) hit_way_conv (.*, .one_hot(tag_hit_way), .int_out(tag_hit_way_int)); - one_hot_to_integer #(DCACHE_WAYS) update_way_conv (.*, .one_hot(replacement_way), .int_out(replacement_way_int)); + one_hot_to_integer #(DCACHE_WAYS) hit_way_conv ( + .clk (clk), + .rst (rst), + .one_hot(tag_hit_way), + .int_out(tag_hit_way_int) + ); + one_hot_to_integer #(DCACHE_WAYS) update_way_conv ( + .clk (clk), + .rst (rst), + .one_hot (replacement_way), + .int_out (replacement_way_int) + ); //If atomic load (LR or AMO op) and there's a tag hit reuse same line @@ -190,17 +205,21 @@ module dcache( //////////////////////////////////////////////////// //Tag banks - dtag_banks dcache_tag_banks (.*, - .stage1_addr(ls_inputs.addr), - .stage2_addr(stage2_addr), - .inv_addr({l1_response.inv_addr, 2'b00}), - .update_way(tag_update_way), - .update(tag_update), - .stage1_adv(ls.new_request), - .stage1_inv(1'b0),//For software invalidation - .extern_inv(l1_response.inv_valid), - .extern_inv_complete(l1_response.inv_ack) - ); + dtag_banks dcache_tag_banks ( + .clk (clk), + .rst (rst), + .stage1_addr (ls_inputs.addr), + .stage2_addr (stage2_addr), + .inv_addr ({l1_response.inv_addr, 2'b00}), + .update_way (tag_update_way), + .update (tag_update), + .stage1_adv (ls.new_request), + .stage1_inv (1'b0),//For software invalidation + .extern_inv (l1_response.inv_valid), + .extern_inv_complete (l1_response.inv_ack), + .tag_hit (tag_hit), + .tag_hit_way (tag_hit_way) + ); //////////////////////////////////////////////////// //AMO logic @@ -213,7 +232,10 @@ module dcache( assign amo_alu_inputs.op = stage2_amo.op; generate if (USE_AMO) - amo_alu amo_unit (.*, .result(amo_result)); + amo_alu amo_unit ( + .amo_alu_inputs (amo_alu_inputs), + .result (amo_result) + ); endgenerate always_comb begin @@ -302,4 +324,4 @@ module dcache( assert property (@(posedge clk) disable iff (rst) ls.new_request |-> ls.ready) else $error("dcache received request when not ready"); -endmodule \ No newline at end of file +endmodule diff --git a/core/div_unit.sv b/core/div_unit.sv index 87f0b63..40adeac 100755 --- a/core/div_unit.sv +++ b/core/div_unit.sv @@ -104,7 +104,11 @@ module div_unit //////////////////////////////////////////////////// //Input FIFO taiga_fifo #(.DATA_WIDTH($bits(div_fifo_inputs_t)), .FIFO_DEPTH(1)) - div_input_fifo (.fifo(input_fifo), .*); + div_input_fifo ( + .clk (clk), + .rst (rst), + .fifo (input_fifo) + ); assign input_fifo.data_in = fifo_inputs; assign input_fifo.push = issue.new_request; @@ -134,7 +138,11 @@ module div_unit //Div core assign div_core.dividend = div_op.unsigned_dividend; assign div_core.divisor = div_op.unsigned_divisor; - div_algorithm divider_block (.*, .div(div_core)); + div_algorithm divider_block ( + .clk (clk), + .rst (rst), + .div (div_core) + ); //////////////////////////////////////////////////// //Output diff --git a/core/dtag_banks.sv b/core/dtag_banks.sv index 1ab817c..5efa6bb 100755 --- a/core/dtag_banks.sv +++ b/core/dtag_banks.sv @@ -107,15 +107,19 @@ module dtag_banks( for (i=0; i < DCACHE_WAYS; i=i+1) begin : dtag_bank_gen assign update_tag_way[i] = update_way[i] | (inv_hit_way[i] & extern_inv_complete); - tag_bank #($bits(dtag_entry_t), DCACHE_LINES) dtag_bank (.*, - .en_a(stage1_adv), .wen_a(stage1_inv), - .addr_a(getLineAddr(stage1_addr)), - .data_in_a('0), .data_out_a(tag_line[i]), - - .en_b(miss_or_extern_invalidate), .wen_b(update_tag_way[i]), - .addr_b(update_port_addr), - .data_in_b(new_tagline), .data_out_b(inv_tag_line[i]) - ); + tag_bank #($bits(dtag_entry_t), DCACHE_LINES) dtag_bank ( + .clk (clk), + .rst (rst), + .en_a (stage1_adv), + .wen_a (stage1_inv), + .addr_a (getLineAddr(stage1_addr)), + .data_in_a ('0), + .data_out_a (tag_line[i]), + .en_b (miss_or_extern_invalidate), + .wen_b (update_tag_way[i]), + .addr_b (update_port_addr), + .data_in_b (new_tagline), .data_out_b(inv_tag_line[i]) + ); assign inv_hit_way[i] = (inv_hit_comparison_tagline == inv_tag_line[i]); assign tag_hit_way[i] = (stage2_hit_comparison_tagline == tag_line[i]); diff --git a/core/external_interfaces.sv b/core/external_interfaces.sv index 64139ab..e029f2d 100644 --- a/core/external_interfaces.sv +++ b/core/external_interfaces.sv @@ -82,6 +82,12 @@ interface axi_interface; wready, bvalid, bresp, bid); + modport formal (input arready, arvalid, araddr, arlen, arsize, arburst, arcache, + rready, rvalid, rdata, rresp, rlast, rid, + awready, awvalid, awaddr, awlen, awsize, awburst, awcache, arid, + wready, wvalid, wdata, wstrb, wlast, awid, + bready, bvalid, bresp, bid); + endinterface interface avalon_interface; @@ -99,6 +105,8 @@ interface avalon_interface; output addr, read, write, byteenable, writedata); modport slave (output readdata, waitrequest, readdatavalid, writeresponsevalid, input addr, read, write, byteenable, writedata); + modport formal (input readdata, waitrequest, readdatavalid, writeresponsevalid, + addr, read, write, byteenable, writedata); endinterface @@ -116,6 +124,7 @@ interface wishbone_interface; output addr, we, sel, writedata, stb, cyc); modport slave (output readdata, ack, input addr, we, sel, writedata, stb, cyc); + modport formal (input readdata, ack, addr, we, sel, writedata, stb, cyc); endinterface @@ -142,6 +151,7 @@ interface l1_arbiter_request_interface; modport master (output addr, data, rnw, be, size, is_amo, amo, request, input ack); modport slave (import to_l2, input addr, data, rnw, be, size, is_amo, amo, request, output ack); + modport formal (input addr, data, rnw, be, size, is_amo, amo, request, ack); endinterface @@ -154,6 +164,7 @@ interface l1_arbiter_return_interface; modport master (input inv_addr, inv_valid, data, data_valid, output inv_ack); modport slave (output inv_addr, inv_valid, data, data_valid, input inv_ack); + modport formal (input inv_addr, inv_valid, data, data_valid, inv_ack); endinterface diff --git a/core/fetch.sv b/core/fetch.sv index 9d1b029..b82ec9f 100755 --- a/core/fetch.sv +++ b/core/fetch.sv @@ -147,13 +147,22 @@ module fetch( assign fetch_attr_fifo.push = new_mem_request; assign fetch_attr_fifo.potential_push = new_mem_request; assign fetch_attr_fifo.pop = fetch_complete; - one_hot_to_integer #(NUM_SUB_UNITS) hit_way_conv (.*, .one_hot(sub_unit_address_match), .int_out(fetch_attr_next.subunit_id)); + one_hot_to_integer #(NUM_SUB_UNITS) hit_way_conv ( + .clk (clk), + .rst (rst), + .one_hot (sub_unit_address_match), + .int_out (fetch_attr_next.subunit_id) + ); assign fetch_attr_next.address_valid = |sub_unit_address_match; assign fetch_attr_fifo.data_in = fetch_attr_next; taiga_fifo #(.DATA_WIDTH($bits(fetch_attributes_t)), .FIFO_DEPTH(NEXT_ID_DEPTH)) - attributes_fifo (.fifo(fetch_attr_fifo), .rst(flush_or_rst), .*); + attributes_fifo ( + .clk (clk), + .rst (flush_or_rst), + .fifo (fetch_attr_fifo) + ); assign fetch_attr = fetch_attr_fifo.data_out; @@ -176,12 +185,24 @@ module fetch( assign units_ready = &unit_ready; generate if (USE_I_SCRATCH_MEM) begin - ibram i_bram (.*, .fetch_sub(fetch_sub[BRAM_ID])); + ibram i_bram ( + .clk (clk), + .rst (rst), + .fetch_sub (fetch_sub[BRAM_ID]), + .instruction_bram (instruction_bram) + ); assign sub_unit_address_match[BRAM_ID] = tlb.physical_address[31:32-SCRATCH_BIT_CHECK] == SCRATCH_ADDR_L[31:32-SCRATCH_BIT_CHECK]; end endgenerate generate if (USE_ICACHE) begin - icache i_cache (.*, .fetch_sub(fetch_sub[ICACHE_ID])); + icache i_cache ( + .clk (clk), + .rst (rst), + .icache_on (icache_on), + .l1_request (l1_request), + .l1_response (l1_response), + .fetch_sub (fetch_sub[ICACHE_ID]) + ); assign sub_unit_address_match[ICACHE_ID] = tlb.physical_address[31:32-MEMORY_BIT_CHECK] == MEMORY_ADDR_L[31:32-MEMORY_BIT_CHECK]; end endgenerate @@ -203,4 +224,4 @@ module fetch( assert property (@(posedge clk) disable iff (rst) (|unit_data_valid) |-> (fetch_attr_fifo.valid && unit_data_valid[fetch_attr.subunit_id])) else $error("Spurious fetch complete detected!"); -endmodule \ No newline at end of file +endmodule diff --git a/core/gc_unit.sv b/core/gc_unit.sv index e4a49f6..c81dcfb 100644 --- a/core/gc_unit.sv +++ b/core/gc_unit.sv @@ -240,8 +240,19 @@ module gc_unit( end //Counters for tlb clearing states - shift_counter #(.DEPTH(INIT_CLEAR_DEPTH)) init_clear_counter (.*, .start((state == PRE_CLEAR_STATE)), .done(init_clear_done)); - shift_counter #(.DEPTH(TLB_CLEAR_DEPTH)) tlb_clear_counter (.*, .start((state == IDLE_STATE) && (next_state == TLB_CLEAR_STATE)), .done(tlb_clear_done)); + shift_counter #(.DEPTH(INIT_CLEAR_DEPTH)) init_clear_counter ( + .clk (clk), + .rst (rst), + .start ((state == PRE_CLEAR_STATE)), + .done (init_clear_done) + ); + + shift_counter #(.DEPTH(TLB_CLEAR_DEPTH)) tlb_clear_counter ( + .clk (clk), + .rst (rst), + .start ((state == IDLE_STATE) && (next_state == TLB_CLEAR_STATE)), + .done (tlb_clear_done) + ); //////////////////////////////////////////////////// //mret/sret @@ -376,4 +387,4 @@ module gc_unit( end endgenerate `endif -endmodule \ No newline at end of file +endmodule diff --git a/core/icache.sv b/core/icache.sv index 689813f..702c149 100755 --- a/core/icache.sv +++ b/core/icache.sv @@ -90,7 +90,12 @@ module icache end //Replacement policy is psuedo random - cycler #(ICACHE_WAYS) replacement_policy (.*, .en(1'b1), .one_hot(replacement_way)); + cycler #(ICACHE_WAYS) replacement_policy ( + .clk (clk), + .rst (rst), + .en (1'b1), + .one_hot (replacement_way) + ); always_ff @ (posedge clk) begin if (second_cycle) tag_update_way <= replacement_way; diff --git a/core/instruction_metadata_and_id_management.sv b/core/instruction_metadata_and_id_management.sv index 8d07d59..1776580 100644 --- a/core/instruction_metadata_and_id_management.sv +++ b/core/instruction_metadata_and_id_management.sv @@ -113,6 +113,9 @@ module instruction_metadata_and_id_management logic [$clog2(MAX_COMPLETE_COUNT)-1:0] complete_count; + logic id_not_in_decode_issue; + logic id_not_inflight; + //Writes to register file id_t rd_to_id_table [32]; genvar i; @@ -292,8 +295,7 @@ module instruction_metadata_and_id_management end endgenerate //Computed one cycle in advance using pc_id_next - logic id_not_in_decode_issue; - logic id_not_inflight; + assign id_not_in_decode_issue = ~(decoded_status ^ decoded_issued_status); assign id_not_inflight = ~(issued_status ^ @@ -386,4 +388,4 @@ module instruction_metadata_and_id_management assert property (@(posedge clk) disable iff (rst) !(~decode.valid & decode_advance)) else $error("Decode advanced without ID"); -endmodule \ No newline at end of file +endmodule diff --git a/core/load_store_unit.sv b/core/load_store_unit.sv index 2e2eade..4248f99 100755 --- a/core/load_store_unit.sv +++ b/core/load_store_unit.sv @@ -191,7 +191,15 @@ endgenerate assign lsq.new_issue = issue.new_request & ~unaligned_addr; logic [MAX_IDS-1:0] wb_hold_for_store_ids; - load_store_queue lsq_block (.*); + load_store_queue lsq_block ( + .clk (clk), + .rst (rst), + .gc_fetch_flush (gc_fetch_flush), + .gc_issue_flush (gc_issue_flush), + .lsq (lsq), + .wb_store (wb_store), + .ready_for_forwarded_store (ready_for_forwarded_store) + ); assign shared_inputs = lsq.transaction_out; assign lsq.accepted = issue_request; @@ -234,8 +242,17 @@ endgenerate //////////////////////////////////////////////////// //Load attributes FIFO - one_hot_to_integer #(NUM_SUB_UNITS) sub_unit_select (.*, .one_hot(sub_unit_address_match), .int_out(load_attributes_in.subunit_id)); - taiga_fifo #(.DATA_WIDTH($bits(load_attributes_t)), .FIFO_DEPTH(ATTRIBUTES_DEPTH)) attributes_fifo (.fifo(load_attributes), .*); + one_hot_to_integer #(NUM_SUB_UNITS) sub_unit_select ( + .clk (clk), + .rst (rst), + .one_hot (sub_unit_address_match), + .int_out (load_attributes_in.subunit_id) + ); + taiga_fifo #(.DATA_WIDTH($bits(load_attributes_t)), .FIFO_DEPTH(ATTRIBUTES_DEPTH)) attributes_fifo ( + .clk (clk), + .rst (rst), + .fifo (load_attributes) + ); assign load_attributes_in.fn3 = shared_inputs.fn3; assign load_attributes_in.byte_addr = shared_inputs.addr[1:0]; assign load_attributes_in.id = shared_inputs.id; @@ -256,7 +273,14 @@ endgenerate assign unit_ready[BRAM_ID] = bram.ready; assign unit_data_valid[BRAM_ID] = bram.data_valid; - dbram d_bram (.*, .ls_inputs(shared_inputs), .ls(bram), .data_out(unit_data_array[BRAM_ID])); + dbram d_bram ( + .clk (clk), + .rst (rst), + .ls_inputs (shared_inputs), + .ls (bram), + .data_out (unit_data_array[BRAM_ID]), + .data_bram (data_bram) + ); end endgenerate @@ -268,11 +292,34 @@ endgenerate assign unit_data_valid[BUS_ID] = bus.data_valid; if(BUS_TYPE == AXI_BUS) - axi_master axi_bus (.*, .ls_inputs(shared_inputs), .size({1'b0,shared_inputs.fn3[1:0]}), .m_axi(m_axi), .ls(bus), .data_out(unit_data_array[BUS_ID])); //Lower two bits of fn3 match AXI specification for request size (byte/halfword/word) + axi_master axi_bus ( + .clk (clk), + .rst (rst), + .m_axi (m_axi), + .size ({1'b0,shared_inputs.fn3[1:0]}), + .data_out (unit_data_array[BUS_ID]), + .ls_inputs (shared_inputs), + .ls (bus) + ); //Lower two bits of fn3 match AXI specification for request size (byte/halfword/word) + else if (BUS_TYPE == WISHBONE_BUS) - wishbone_master wishbone_bus (.*, .ls_inputs(shared_inputs), .m_wishbone(m_wishbone), .ls(bus), .data_out(unit_data_array[BUS_ID])); + wishbone_master wishbone_bus ( + .clk (clk), + .rst (rst), + .m_wishbone (m_wishbone), + .data_out (unit_data_array[BUS_ID]), + .ls_inputs (shared_inputs), + .ls (bus) + ); else if (BUS_TYPE == AVALON_BUS) begin - avalon_master avalon_bus (.*, .ls_inputs(shared_inputs), .m_avalon(m_avalon), .ls(bus), .data_out(unit_data_array[BUS_ID])); + avalon_master avalon_bus ( + .clk (clk), + .rst (rst), + .ls_inputs (shared_inputs), + .m_avalon (m_avalon), + .ls (bus), + .data_out (unit_data_array[BUS_ID]) + ); end end endgenerate @@ -284,7 +331,20 @@ endgenerate assign unit_ready[DCACHE_ID] = cache.ready; assign unit_data_valid[DCACHE_ID] = cache.data_valid; - dcache data_cache (.*, .ls_inputs(shared_inputs), .ls(cache), .amo(ls_inputs.amo), .data_out(unit_data_array[DCACHE_ID])); + dcache data_cache ( + .clk (clk), + .rst (rst), + .dcache_on (dcache_on), + .l1_request (l1_request), + .l1_response (l1_response), + .sc_complete (sc_complete), + .sc_success (sc_success), + .clear_reservation (clear_reservation), + .ls_inputs (shared_inputs), + .data_out (unit_data_array[DCACHE_ID]), + .amo (ls_inputs.amo), + .ls (cache) + ); end endgenerate @@ -341,4 +401,4 @@ endgenerate else $error("invalid L/S address"); `endif -endmodule \ No newline at end of file +endmodule diff --git a/core/shift_counter.sv b/core/shift_counter.sv index 0d615d3..2cf21ff 100644 --- a/core/shift_counter.sv +++ b/core/shift_counter.sv @@ -25,7 +25,7 @@ import taiga_types::*; module shift_counter #(parameter DEPTH = 16) ( input logic clk, - + input logic rst, input logic start, output logic done ); diff --git a/core/taiga.sv b/core/taiga.sv index 29e74db..abe6471 100755 --- a/core/taiga.sv +++ b/core/taiga.sv @@ -190,21 +190,119 @@ module taiga ( //////////////////////////////////////////////////// // Memory Interface generate if (ENABLE_S_MODE || USE_ICACHE || USE_DCACHE) - l1_arbiter arb(.*); + + l1_arbiter arb( + .clk (clk), + .rst (rst), + .l2 (l2), + .sc_complete (sc_complete), + .sc_success (sc_success), + .l1_request (l1_request), + .l1_response (l1_response) + ); + endgenerate //////////////////////////////////////////////////// // ID support - instruction_metadata_and_id_management id_block (.*); + instruction_metadata_and_id_management id_block ( + .clk (clk), + .rst (rst), + .gc_init_clear (gc_init_clear), + .gc_fetch_flush (gc_fetch_flush), + .pc_id (pc_id), + .pc_id_available (pc_id_available), + .if_pc (if_pc), + .pc_id_assigned (pc_id_assigned), + .fetch_id (fetch_id), + .fetch_complete (fetch_complete), + .fetch_instruction (fetch_instruction), + .fetch_address_valid (fetch_address_valid), + .decode (decode), + .decode_advance (decode_advance), + .issue (issue), + .instruction_issued (instruction_issued), + .rs_id (rs_id), + .rs_inuse (rs_inuse), + .rs_id_inuse (rs_id_inuse), + .branch_metadata_if (branch_metadata_if), + .branch_metadata_ex (branch_metadata_ex), + .store_complete (store_complete), + .store_id (store_id), + .branch_complete (branch_complete), + .branch_id (branch_id), + .system_op_or_exception_complete (system_op_or_exception_complete), + .exception_with_rd_complete (exception_with_rd_complete), + .system_op_or_exception_id (system_op_or_exception_id), + .retire_inc (retire_inc), + .ids_retiring (ids_retiring), + .retired (retired), + .retired_rd_addr (retired_rd_addr), + .id_for_rd (id_for_rd), + .exception_pc (exception_pc) + ); //////////////////////////////////////////////////// // Fetch - fetch fetch_block (.*, .icache_on('1), .tlb(itlb), .l1_request(l1_request[L1_ICACHE_ID]), .l1_response(l1_response[L1_ICACHE_ID]), .exception(1'b0)); - branch_predictor bp_block (.*); - ras ras_block(.*); + fetch fetch_block ( + .clk (clk), + .rst (rst), + .branch_flush (branch_flush), + .gc_fetch_hold (gc_fetch_hold), + .gc_fetch_flush (gc_fetch_flush), + .gc_fetch_pc_override (gc_fetch_pc_override), + .gc_fetch_pc (gc_fetch_pc), + .pc_id_available (pc_id_available), + .pc_id_assigned (pc_id_assigned), + .fetch_complete (fetch_complete), + .fetch_address_valid (fetch_address_valid), + .bp (bp), + .ras (ras), + .if_pc (if_pc), + .fetch_instruction (fetch_instruction), + .instruction_bram (instruction_bram), + .icache_on('1), .tlb(itlb), + .l1_request(l1_request[L1_ICACHE_ID]), + .l1_response(l1_response[L1_ICACHE_ID]), + .exception(1'b0) + ); + + branch_predictor bp_block ( + .clk (clk), + .rst (rst), + .bp (bp), + .branch_metadata_if (branch_metadata_if), + .branch_metadata_ex (branch_metadata_ex), + .br_results (br_results) + ); + + ras ras_block( + .clk (clk), + .rst (rst), + .gc_fetch_flush (gc_fetch_flush), + .ras (ras) + ); + generate if (ENABLE_S_MODE) begin - tlb_lut_ram #(ITLB_WAYS, ITLB_DEPTH) i_tlb (.*, .tlb(itlb), .mmu(immu)); - mmu i_mmu (.*, .mmu(immu) , .l1_request(l1_request[L1_IMMU_ID]), .l1_response(l1_response[L1_IMMU_ID]), .mmu_exception()); + + tlb_lut_ram #(ITLB_WAYS, ITLB_DEPTH) i_tlb ( + .clk (clk), + .rst (rst), + .tlb_on (tlb_on), + .asid (asid), + .tlb (itlb), + .mmu (immu) + ); + + mmu i_mmu ( + .clk (clk), + .rst (rst), + .mmu (immu) , + .l1_request (l1_request[L1_IMMU_ID]), + .l1_response (l1_response[L1_IMMU_ID]), + .mmu_exception () + ); + end else begin assign itlb.complete = 1; @@ -214,33 +312,220 @@ module taiga ( //////////////////////////////////////////////////// //Decode/Issue - decode_and_issue decode_and_issue_block (.*); + decode_and_issue decode_and_issue_block ( + .clk (clk), + .rst (rst), + .decode (decode), + .decode_advance (decode_advance), + .issue (issue), + .rs_data (rs_data), + .alu_inputs (alu_inputs), + .ls_inputs (ls_inputs), + .branch_inputs (branch_inputs), + .gc_inputs (gc_inputs), + .mul_inputs (mul_inputs), + .div_inputs (div_inputs), + .unit_issue (unit_issue), + .potential_branch_exception (potential_branch_exception), + .alu_issued (alu_issued), + .gc_fetch_hold (gc_fetch_hold), + .gc_issue_hold (gc_issue_hold), + .gc_fetch_flush (gc_fetch_flush), + .gc_issue_flush (gc_issue_flush), + .gc_flush_required (gc_flush_required), + .rs_inuse (rs_inuse), + .rs_id (rs_id), + .rs_id_inuse (rs_id_inuse), + .instruction_issued (instruction_issued), + .illegal_instruction (illegal_instruction), + .tr_operand_stall (tr_operand_stall), + .tr_unit_stall (tr_unit_stall), + .tr_no_id_stall (tr_no_id_stall), + .tr_no_instruction_stall (tr_no_instruction_stall), + .tr_other_stall (tr_other_stall), + .tr_branch_operand_stall (tr_branch_operand_stall), + .tr_alu_operand_stall (tr_alu_operand_stall), + .tr_ls_operand_stall (tr_ls_operand_stall), + .tr_div_operand_stall (tr_div_operand_stall), + .tr_alu_op (tr_alu_op), + .tr_branch_or_jump_op (tr_branch_or_jump_op), + .tr_load_op (tr_load_op), + .tr_store_op (tr_store_op), + .tr_mul_op (tr_mul_op), + .tr_div_op (tr_div_op), + .tr_misc_op (tr_misc_op), + .tr_instruction_issued_dec (tr_instruction_issued_dec), + .tr_instruction_pc_dec (tr_instruction_pc_dec), + .tr_instruction_data_dec (tr_instruction_data_dec) + ); //////////////////////////////////////////////////// //Register File and Writeback - register_file_and_writeback register_file_and_writeback_block (.*); + register_file_and_writeback register_file_and_writeback_block ( + .clk (clk), + .rst (rst), + .issue (issue), + .alu_issued (alu_issued), + .rs_data (rs_data), + .ids_retiring (ids_retiring), + .retired (retired), + .retired_rd_addr (retired_rd_addr), + .id_for_rd (id_for_rd), + .unit_wb (unit_wb), + .wb_store (wb_store), + .tr_rs1_forwarding_needed (tr_rs1_forwarding_needed), + .tr_rs2_forwarding_needed (tr_rs2_forwarding_needed), + .tr_rs1_and_rs2_forwarding_needed (tr_rs1_and_rs2_forwarding_needed) + ); //////////////////////////////////////////////////// //Execution Units - branch_unit branch_unit_block (.*, .issue(unit_issue[BRANCH_UNIT_ID])); - alu_unit alu_unit_block (.*, .issue(unit_issue[ALU_UNIT_WB_ID]), .wb(unit_wb[ALU_UNIT_WB_ID])); - load_store_unit load_store_unit_block (.*, .dcache_on(1'b1), .clear_reservation(1'b0), .tlb(dtlb), .issue(unit_issue[LS_UNIT_WB_ID]), .wb(unit_wb[LS_UNIT_WB_ID]), .l1_request(l1_request[L1_DCACHE_ID]), .l1_response(l1_response[L1_DCACHE_ID])); + branch_unit branch_unit_block ( + .clk (clk ), + .rst (rst ), + .issue (unit_issue[BRANCH_UNIT_ID]), + .branch_inputs (branch_inputs ), + .br_results (br_results ), + .ras (ras ), + .branch_flush (branch_flush ), + .branch_complete (branch_complete ), + .branch_id (branch_id ), + .branch_metadata_ex (branch_metadata_ex ), + .potential_branch_exception (potential_branch_exception), + .branch_exception_is_jump (branch_exception_is_jump ), + .br_exception (br_exception ), + .tr_branch_correct (tr_branch_correct ), + .tr_branch_misspredict (tr_branch_misspredict ), + .tr_return_correct (tr_return_correct ), + .tr_return_misspredict (tr_return_misspredict ) + ); + + + alu_unit alu_unit_block ( + .clk (clk), + .rst (rst), + .alu_inputs (alu_inputs), + .issue (unit_issue[ALU_UNIT_WB_ID]), + .wb (unit_wb[ALU_UNIT_WB_ID]) + ); + + load_store_unit load_store_unit_block ( + .clk (clk), + .rst (rst), + .ls_inputs (ls_inputs), + .issue (unit_issue[LS_UNIT_WB_ID]), + .dcache_on (1'b1), + .clear_reservation (1'b0), + .tlb (dtlb), + .gc_fetch_flush (gc_fetch_flush), + .gc_issue_flush (gc_issue_flush), + .l1_request (l1_request[L1_DCACHE_ID]), + .l1_response (l1_response[L1_DCACHE_ID]), + .sc_complete (sc_complete), + .sc_success (sc_success), + .m_axi (m_axi), + .m_avalon (m_avalon), + .m_wishbone (m_wishbone), + .data_bram (data_bram), + .store_complete (store_complete), + .store_id (store_id), + .wb_store (wb_store), + .csr_rd (csr_rd), + .csr_id (csr_id), + .csr_done (csr_done), + .ls_is_idle (ls_is_idle), + .ls_exception (ls_exception), + .ls_exception_is_store (ls_exception_is_store), + .wb (unit_wb[LS_UNIT_WB_ID]) + ); + generate if (ENABLE_S_MODE) begin - tlb_lut_ram #(DTLB_WAYS, DTLB_DEPTH) d_tlb (.*, .tlb(dtlb), .mmu(dmmu)); - mmu d_mmu (.*, .mmu(dmmu), .l1_request(l1_request[L1_DMMU_ID]), .l1_response(l1_response[L1_DMMU_ID]), .mmu_exception()); - end - else begin + + tlb_lut_ram #(DTLB_WAYS, DTLB_DEPTH) d_tlb ( + .clk (clk), + .rst (rst), + .tlb_on (tlb_on), + .asid (asid), + .tlb (dtlb), + .mmu (dmmu) + ); + + mmu d_mmu ( + .clk (clk), + .rst (rst), + .mmu (dmmu) , + .l1_request (l1_request[L1_DMMU_ID]), + .l1_response (l1_response[L1_DMMU_ID]), + .mmu_exception () + ); + end + else begin assign dtlb.complete = 1; assign dtlb.physical_address = dtlb.virtual_address; - end + end endgenerate - gc_unit gc_unit_block (.*, .issue(unit_issue[GC_UNIT_ID])); + gc_unit gc_unit_block ( + .clk (clk), + .rst (rst), + .issue (unit_issue[GC_UNIT_ID]), + .gc_inputs (gc_inputs), + .gc_flush_required (gc_flush_required), + .branch_flush (branch_flush), + .potential_branch_exception (potential_branch_exception), + .branch_exception_is_jump (branch_exception_is_jump), + .br_exception (br_exception), + .illegal_instruction (illegal_instruction), + .ls_exception (ls_exception), + .ls_exception_is_store (ls_exception_is_store), + .tlb_on (tlb_on), + .asid (asid), + .immu (immu), + .dmmu (dmmu), + .system_op_or_exception_complete (system_op_or_exception_complete), + .exception_with_rd_complete (exception_with_rd_complete), + .system_op_or_exception_id (system_op_or_exception_id), + .exception_pc (exception_pc), + .retire_inc (retire_inc), + .instruction_retired (instruction_retired), + .interrupt (interrupt), + .timer_interrupt (timer_interrupt), + .gc_init_clear (gc_init_clear), + .gc_fetch_hold (gc_fetch_hold), + .gc_issue_hold (gc_issue_hold), + .gc_issue_flush (gc_issue_flush), + .gc_fetch_flush (gc_fetch_flush), + .gc_fetch_pc_override (gc_fetch_pc_override), + .gc_supress_writeback (gc_supress_writeback), + .gc_fetch_pc (gc_fetch_pc), + .csr_rd (csr_rd), + .csr_id (csr_id), + .csr_done (csr_done), + .ls_is_idle (ls_is_idle) + ); generate if (USE_MUL) - mul_unit mul_unit_block (.*, .issue(unit_issue[MUL_UNIT_WB_ID]), .wb(unit_wb[MUL_UNIT_WB_ID])); + + mul_unit mul_unit_block (.*, + .clk (clk), + .rst (rst), + .mul_inputs (mul_inputs), + .issue (unit_issue[MUL_UNIT_WB_ID]), + .wb (unit_wb[MUL_UNIT_WB_ID]) + ); + endgenerate + generate if (USE_DIV) - div_unit div_unit_block (.*, .issue(unit_issue[DIV_UNIT_WB_ID]), .wb(unit_wb[DIV_UNIT_WB_ID])); + + div_unit div_unit_block ( + .clk (clk), + .rst (rst), + .gc_fetch_flush (gc_fetch_flush), + .div_inputs (div_inputs), + .issue (unit_issue[DIV_UNIT_WB_ID]), + .wb (unit_wb[DIV_UNIT_WB_ID]) + ); + endgenerate //////////////////////////////////////////////////// diff --git a/core/tlb_lut_ram.sv b/core/tlb_lut_ram.sv index f47c8cf..0d6f8fa 100755 --- a/core/tlb_lut_ram.sv +++ b/core/tlb_lut_ram.sv @@ -88,7 +88,12 @@ module tlb_lut_ram #( end endgenerate - cycler #(.C_WIDTH(WAYS)) replacement_policy (.*, .en(1'b1), .one_hot(replacement_way)); + cycler #(.C_WIDTH(WAYS)) replacement_policy ( + .clk (clk), + .rst (rst), + .en (1'b1), + .one_hot (replacement_way) + ); always_ff @ (posedge clk) begin diff --git a/formal/scripts/setup_taiga_dev.tcl b/formal/scripts/setup_taiga_dev.tcl index 3e2bcc0..92e23b3 100644 --- a/formal/scripts/setup_taiga_dev.tcl +++ b/formal/scripts/setup_taiga_dev.tcl @@ -24,8 +24,8 @@ clear -all set_engine_mode {Hp Ht L B I N Tri} -set SCRIPTS_PATH ./Taiga-dev/formal/scripts -set JG_TAIGA_RTL_PATH ./Taiga-dev +set SCRIPTS_PATH ../../Taiga-dev/formal/scripts +set JG_TAIGA_RTL_PATH ../../Taiga-dev analyze -sv -f ${SCRIPTS_PATH}/taiga_rtl.vfile analyze -sv ${JG_TAIGA_RTL_PATH}/formal/models/taiga_fbm.sv diff --git a/l2_arbiter/l2_external_interfaces.sv b/l2_arbiter/l2_external_interfaces.sv index e4b7012..2f9d216 100644 --- a/l2_arbiter/l2_external_interfaces.sv +++ b/l2_arbiter/l2_external_interfaces.sv @@ -63,6 +63,14 @@ interface l2_requester_interface; output con_result, con_valid, input wr_data, wr_data_push, output data_full, output rd_data, rd_sub_id, rd_data_valid, input rd_data_ack); + + modport formal (input addr, be, rnw, is_amo, amo_type_or_burst_size, sub_id, + request_push, output request_full, + inv_addr, inv_valid, input inv_ack, + con_result, con_valid, + wr_data, wr_data_push, output data_full, + rd_data, rd_sub_id, rd_data_valid, input rd_data_ack); + endinterface @@ -96,5 +104,11 @@ interface l2_memory_interface #( parameter L2_ID_W = $clog2(L2_NUM_PORTS) + L2_S input request_valid, abort, output request_pop, input wr_data, wr_data_valid, output wr_data_read, output rd_data, rd_id, rd_data_valid); + + modport formal (input addr, be, rnw, is_amo, amo_type_or_burst_size, id, + request_valid, abort, output request_pop, + wr_data, wr_data_valid, output wr_data_read, + rd_data, rd_id, rd_data_valid); + endinterface diff --git a/l2_arbiter/l2_interfaces.sv b/l2_arbiter/l2_interfaces.sv index b3c207d..4bdda26 100755 --- a/l2_arbiter/l2_interfaces.sv +++ b/l2_arbiter/l2_interfaces.sv @@ -31,4 +31,5 @@ interface l2_arbitration_interface; modport slave (input requests, strobe, output grantee_i, grantee_v , grantee_valid); modport master (output requests, strobe, input grantee_i, grantee_v , grantee_valid); + modport formal (input requests, strobe, output grantee_i, grantee_v , grantee_valid); endinterface diff --git a/local_memory/local_memory_interface.sv b/local_memory/local_memory_interface.sv index 76895fd..61a4bcd 100644 --- a/local_memory/local_memory_interface.sv +++ b/local_memory/local_memory_interface.sv @@ -30,6 +30,7 @@ interface local_memory_interface; modport slave (input addr, en, be, data_in, output data_out); modport master (output addr, en, be, data_in, input data_out); + modport formal (input addr, en, be, data_in, data_out); endinterface