diff --git a/crates/cpu/src/decoder/simple_power_isa.rs b/crates/cpu/src/decoder/simple_power_isa.rs index 91890e2..b78fc28 100644 --- a/crates/cpu/src/decoder/simple_power_isa.rs +++ b/crates/cpu/src/decoder/simple_power_isa.rs @@ -16,6 +16,7 @@ use crate::{ register::{ PRegFlags, PRegFlagsPowerISA, PRegFlagsPowerISAView, PRegFlagsViewTrait, ViewUnused, }, + test::decode_and_run_single_insn::{DecodeOneInsn, DecodeOneInsnOutput}, util::{ Rotate, array_vec::{ArrayVec, Length}, @@ -138,7 +139,7 @@ struct DecodeState<'a> { conditions: Option<&'static str>, header: &'static crate::powerisa_instructions_xml::InstructionHeader, insn: &'static crate::powerisa_instructions_xml::Instruction, - output: Expr>>, + output: Expr, ConstUsize<3>>>, is_illegal: Expr, first_input: Expr>, second_input: Expr>>, @@ -594,7 +595,7 @@ impl DecodeState<'_> { 1usize.cast_to_static::>(), ); connect( - this.output[0], + *this.output[0], BranchMOp::branch_i( MOpDestReg::new( [if this.mnemonic.contains('l') { @@ -701,7 +702,7 @@ impl DecodeState<'_> { ArrayVec::len(this.output), 1usize.cast_to_static::>(), ); - connect(this.output[0], branch_mop); + connect(*this.output[0], branch_mop); connect(branch_ctr_reg, MOpRegNum::const_zero()); } else { connect( @@ -709,7 +710,7 @@ impl DecodeState<'_> { 2usize.cast_to_static::>(), ); connect( - this.output[0], + *this.output[0], AddSubMOp::add_sub_i( MOpDestReg::new([MOpRegNum::power_isa_ctr_reg()], []), [MOpRegNum::power_isa_ctr_reg(), MOpRegNum::const_zero()], @@ -721,7 +722,7 @@ impl DecodeState<'_> { false, ), ); - connect(this.output[1], branch_mop); + connect(*this.output[1], branch_mop); connect(branch_ctr_reg, MOpRegNum::power_isa_ctr_reg()); } }; @@ -782,7 +783,7 @@ impl DecodeState<'_> { - bt_flag_index.cast_to(uint_ty)) % PRegFlags::FLAG_COUNT; connect( - this.output[0], + *this.output[0], LogicalFlagsMOp::logical_flags( MOpDestReg::new([bt_reg], []), [ba_reg, bb_reg, bt_reg], @@ -808,7 +809,7 @@ impl DecodeState<'_> { 1usize.cast_to_static::>(), ); connect( - this.output[0], + *this.output[0], MoveRegMOp::move_reg( MOpDestReg::new([crf(bf)], []), [crf(bfa)], @@ -885,7 +886,7 @@ impl DecodeState<'_> { #[hdl] if r { connect( - this.output[0], + *this.output[0], AddSubMOp::add_sub_i( MOpDestReg::new([ea_reg], []), [MOpRegNum::const_zero(); 2], @@ -899,7 +900,7 @@ impl DecodeState<'_> { ); } else { connect( - this.output[0], + *this.output[0], AddSubMOp::add_sub_i( MOpDestReg::new([ea_reg], []), [gpr_or_zero(ra), MOpRegNum::const_zero()], @@ -913,7 +914,7 @@ impl DecodeState<'_> { ); } connect( - this.output[1], + *this.output[1], LoadMOp::load(MOpDestReg::new([gpr(rt)], []), [ea_reg], width, conversion), ); }, @@ -927,7 +928,7 @@ impl DecodeState<'_> { ); let ea_reg = ea_reg(ra); connect( - this.output[0], + *this.output[0], AddSubMOp::add_sub_i( MOpDestReg::new([ea_reg], []), [gpr_or_zero(ra), gpr(rb)], @@ -940,7 +941,7 @@ impl DecodeState<'_> { ), ); connect( - this.output[1], + *this.output[1], LoadMOp::load(MOpDestReg::new([gpr(rt)], []), [ea_reg], width, conversion), ); }); @@ -952,7 +953,7 @@ impl DecodeState<'_> { ); let ea_reg = ea_reg(ra); connect( - this.output[0], + *this.output[0], AddSubMOp::add_sub_i( MOpDestReg::new([ea_reg], []), [gpr_or_zero(ra), MOpRegNum::const_zero()], @@ -965,7 +966,7 @@ impl DecodeState<'_> { ), ); connect( - this.output[1], + *this.output[1], LoadMOp::load(MOpDestReg::new([gpr(rt)], []), [ea_reg], width, conversion), ); }); @@ -983,7 +984,7 @@ impl DecodeState<'_> { ); let ea_reg = ea_reg(ra); connect( - this.output[0], + *this.output[0], AddSubMOp::add_sub_i( MOpDestReg::new([ea_reg], []), [gpr_or_zero(ra), MOpRegNum::const_zero()], @@ -996,7 +997,7 @@ impl DecodeState<'_> { ), ); connect( - this.output[1], + *this.output[1], LoadMOp::load(MOpDestReg::new([gpr(rt)], []), [ea_reg], width, conversion), ); }); @@ -1063,9 +1064,9 @@ impl DecodeState<'_> { } else { (MOpRegNum::power_isa_temp_reg(), false.to_expr()) }; - write_compute_ea_insn(this.output[0], ea_reg); + write_compute_ea_insn(*this.output[0], ea_reg); connect( - this.output[1], + *this.output[1], StoreMOp::store( MOpDestReg::new([], []), [ea_reg, gpr(rs)], @@ -1080,7 +1081,7 @@ impl DecodeState<'_> { 3usize.cast_to_static::>(), ); connect( - this.output[2], + *this.output[2], MoveRegMOp::move_reg( MOpDestReg::new([gpr(ra)], []), [ea_reg], @@ -1202,7 +1203,7 @@ impl DecodeState<'_> { 1usize.cast_to_static::>(), ); connect( - this.output[0], + *this.output[0], AddSubMOp::add_sub_i( MOpDestReg::new([gpr(rt)], []), #[hdl] @@ -1225,7 +1226,7 @@ impl DecodeState<'_> { 1usize.cast_to_static::>(), ); connect( - this.output[0], + *this.output[0], AddSubMOp::add_sub_i( MOpDestReg::new([gpr(rt)], []), #[hdl] @@ -1252,7 +1253,7 @@ impl DecodeState<'_> { 1usize.cast_to_static::>(), ); connect( - this.output[0], + *this.output[0], AddSubMOp::add_sub_i( MOpDestReg::new([gpr(rt)], []), #[hdl] @@ -1279,7 +1280,7 @@ impl DecodeState<'_> { + (d1 << 1).cast_to_static::>() + d2.cast_to_static::>(); connect( - this.output[0], + *this.output[0], AddSubMOp::add_sub_i( MOpDestReg::new([gpr(rt)], []), #[hdl] @@ -1306,7 +1307,7 @@ impl DecodeState<'_> { 1usize.cast_to_static::>(), ); connect( - this.output[0], + *this.output[0], AddSubMOp::add_sub( MOpDestReg::new( [gpr(rt)], @@ -1337,7 +1338,7 @@ impl DecodeState<'_> { 1usize.cast_to_static::>(), ); connect( - this.output[0], + *this.output[0], AddSubMOp::add_sub_i( MOpDestReg::new( [gpr(rt), MOpRegNum::power_isa_xer_ca_ca32_reg()], @@ -1369,7 +1370,7 @@ impl DecodeState<'_> { 1usize.cast_to_static::>(), ); connect( - this.output[0], + *this.output[0], AddSubMOp::add_sub( MOpDestReg::new( [ @@ -1406,7 +1407,7 @@ impl DecodeState<'_> { 1usize.cast_to_static::>(), ); connect( - this.output[0], + *this.output[0], AddSubMOp::add_sub_i( MOpDestReg::new( [gpr(rt), MOpRegNum::power_isa_xer_ca_ca32_reg()], @@ -1438,7 +1439,7 @@ impl DecodeState<'_> { 1usize.cast_to_static::>(), ); connect( - this.output[0], + *this.output[0], AddSubMOp::add_sub( MOpDestReg::new( [gpr(rt), MOpRegNum::power_isa_xer_ca_ca32_reg()], @@ -1471,7 +1472,7 @@ impl DecodeState<'_> { 1usize.cast_to_static::>(), ); connect( - this.output[0], + *this.output[0], AddSubMOp::add_sub( MOpDestReg::new( [gpr(rt), MOpRegNum::power_isa_xer_ca_ca32_reg()], @@ -1504,7 +1505,7 @@ impl DecodeState<'_> { 1usize.cast_to_static::>(), ); connect( - this.output[0], + *this.output[0], AddSubMOp::add_sub( MOpDestReg::new( [gpr(rt), MOpRegNum::power_isa_xer_ca_ca32_reg()], @@ -1537,7 +1538,7 @@ impl DecodeState<'_> { 1usize.cast_to_static::>(), ); connect( - this.output[0], + *this.output[0], AddSubMOp::add_sub( MOpDestReg::new( [gpr(rt), MOpRegNum::power_isa_xer_ca_ca32_reg()], @@ -1575,7 +1576,7 @@ impl DecodeState<'_> { 1usize.cast_to_static::>(), ); connect( - this.output[0], + *this.output[0], AddSubMOp::add_sub( MOpDestReg::new( [gpr(rt)], @@ -1615,7 +1616,7 @@ impl DecodeState<'_> { connect(compare_mode, CompareMode.S32()); } connect( - this.output[0], + *this.output[0], CompareMOp::compare_i( MOpDestReg::new([crf(bf)], []), [gpr(ra)], @@ -1643,7 +1644,7 @@ impl DecodeState<'_> { connect(compare_mode, CompareMode.S32()); } connect( - this.output[0], + *this.output[0], CompareMOp::compare( MOpDestReg::new([crf(bf)], []), [gpr(ra), gpr(rb)], @@ -1670,7 +1671,7 @@ impl DecodeState<'_> { connect(compare_mode, CompareMode.U32()); } connect( - this.output[0], + *this.output[0], CompareMOp::compare_i( MOpDestReg::new([crf(bf)], []), [gpr(ra)], @@ -1698,7 +1699,7 @@ impl DecodeState<'_> { connect(compare_mode, CompareMode.U32()); } connect( - this.output[0], + *this.output[0], CompareMOp::compare( MOpDestReg::new([crf(bf)], []), [gpr(ra), gpr(rb)], @@ -1725,7 +1726,7 @@ impl DecodeState<'_> { connect(compare_mode, CompareMode.CmpRBOne()); } connect( - this.output[0], + *this.output[0], CompareMOp::compare( MOpDestReg::new([crf(bf)], []), [gpr(ra), gpr(rb)], @@ -1744,7 +1745,7 @@ impl DecodeState<'_> { 1usize.cast_to_static::>(), ); connect( - this.output[0], + *this.output[0], CompareMOp::compare( MOpDestReg::new([crf(bf)], []), [gpr(ra), gpr(rb)], @@ -1770,7 +1771,7 @@ impl DecodeState<'_> { 1usize.cast_to_static::>(), ); connect( - this.output[0], + *this.output[0], LogicalMOp::logical_i( MOpDestReg::new( [gpr(ra)], @@ -1824,7 +1825,7 @@ impl DecodeState<'_> { 1usize.cast_to_static::>(), ); connect( - this.output[0], + *this.output[0], LogicalMOp::logical( MOpDestReg::new([gpr(ra)], [(MOpRegNum::POWER_ISA_CR_0_REG_NUM, rc)]), [gpr(rs), gpr(rb)], @@ -1838,7 +1839,7 @@ impl DecodeState<'_> { if rs.reg_num.cmp_eq(rb.reg_num) & !rc { // found `mr` connect( - this.output[0], + *this.output[0], MoveRegMOp::move_reg( MOpDestReg::new([gpr(ra)], []), [gpr(rs)], @@ -1867,7 +1868,7 @@ impl DecodeState<'_> { 1usize.cast_to_static::>(), ); connect( - this.output[0], + *this.output[0], LogicalMOp::logical_i( MOpDestReg::new([gpr(ra)], [(MOpRegNum::POWER_ISA_CR_0_REG_NUM, rc)]), [gpr(rs)], @@ -1945,7 +1946,7 @@ impl DecodeState<'_> { ); let dest_logic_op = self.rotate_dest_logic_op(msb0_mask_begin, msb0_mask_end, false); connect( - self.output[0], + *self.output[0], ShiftRotateMOp::shift_rotate( MOpDestReg::new([gpr(ra.0)], [(MOpRegNum::POWER_ISA_CR_0_REG_NUM, rc.0)]), [gpr(rs.0), gpr(rs.0), gpr(rb.0)], @@ -2004,7 +2005,7 @@ impl DecodeState<'_> { } } connect( - self.output[0], + *self.output[0], ShiftRotateMOp::shift_rotate( MOpDestReg::new([gpr(ra.0)], [(MOpRegNum::POWER_ISA_CR_0_REG_NUM, rc.0)]), [gpr(rs.0), gpr(rs.0), rotate_imm_src2], @@ -2156,7 +2157,7 @@ impl DecodeState<'_> { 1usize.cast_to_static::>(), ); connect( - this.output[0], + *this.output[0], ShiftRotateMOp::shift_rotate( MOpDestReg::new( [gpr(ra), MOpRegNum::power_isa_xer_ca_ca32_reg()], @@ -2186,7 +2187,7 @@ impl DecodeState<'_> { 1usize.cast_to_static::>(), ); connect( - this.output[0], + *this.output[0], ShiftRotateMOp::shift_rotate( MOpDestReg::new( [gpr(ra), MOpRegNum::power_isa_xer_ca_ca32_reg()], @@ -2218,7 +2219,7 @@ impl DecodeState<'_> { 1usize.cast_to_static::>(), ); connect( - this.output[0], + *this.output[0], ShiftRotateMOp::shift_rotate( MOpDestReg::new( [ @@ -2280,7 +2281,7 @@ impl DecodeState<'_> { 1usize.cast_to_static::>(), ); connect( - this.output[0], + *this.output[0], ShiftRotateMOp::shift_rotate( MOpDestReg::new([gpr(ra)], [(MOpRegNum::POWER_ISA_CR_0_REG_NUM, rc)]), [gpr(rs), MOpRegNum::const_zero(), MOpRegNum::const_zero()], @@ -2312,7 +2313,7 @@ impl DecodeState<'_> { ); if is_write_to_spr { connect( - self.output[0], + *self.output[0], MoveRegMOp::move_reg( MOpDestReg::new([spr], []), [gpr(reg)], @@ -2321,7 +2322,7 @@ impl DecodeState<'_> { ); } else { connect( - self.output[0], + *self.output[0], MoveRegMOp::move_reg( MOpDestReg::new([gpr(reg)], []), [spr], @@ -2337,7 +2338,7 @@ impl DecodeState<'_> { 1usize.cast_to_static::>(), ); connect( - self.output[0], + *self.output[0], ReadSpecialMOp::read_special( MOpDestReg::new([gpr(reg)], []), [MOpRegNum::const_zero(); 0], @@ -2412,7 +2413,7 @@ impl DecodeState<'_> { 1usize.cast_to_static::>(), ); connect( - this.output[0], + *this.output[0], LogicalFlagsMOp::logical_flags( MOpDestReg::new([crf(bf)], []), [ @@ -2741,10 +2742,12 @@ const DECODE_FNS: &[(&[&str], DecodeFn)] = &[ ), ]; +const MAX_MOPS_PER_INSN: usize = 3; + #[hdl_module] pub fn decode_one_insn() { #[hdl] - let output: ArrayVec> = m.output(); + let output: ArrayVec, ConstUsize<{ MAX_MOPS_PER_INSN }>> = m.output(); #[hdl] let is_illegal: Bool = m.output(); #[hdl] @@ -2816,6 +2819,49 @@ pub fn decode_one_insn() { } } +impl DecodeOneInsn for decode_one_insn { + type Input = (UInt<32>, HdlOption>); + + fn input_ty(self) -> Self::Input { + StaticType::TYPE + } + + type MaxMOpCount = ConstUsize<{ MAX_MOPS_PER_INSN }>; + + fn max_mop_count(self) -> ::SizeType { + ConstUsize + } + + #[hdl] + fn connect_io( + this: Expr, + input: Expr, + output: Expr>, + ) { + #[hdl] + let (first_input, second_input) = input; + connect(this.first_input, first_input); + connect(this.second_input, second_input); + #[hdl] + let size_in_bytes = wire(); + #[hdl] + if this.second_input_used { + connect(size_in_bytes, 8_hdl_u4); + } else { + connect(size_in_bytes, 4_hdl_u4); + } + connect( + output, + #[hdl] + DecodeOneInsnOutput::<_> { + mops: this.output, + size_in_bytes, + is_illegal: this.is_illegal, + }, + ); + } +} + #[hdl_module] pub fn simple_power_isa_decoder(config: PhantomConst) { todo!() diff --git a/crates/cpu/src/instruction.rs b/crates/cpu/src/instruction.rs index d207720..ae2d189 100644 --- a/crates/cpu/src/instruction.rs +++ b/crates/cpu/src/instruction.rs @@ -115,7 +115,7 @@ pub trait MOpTrait: Type { input: &mut SimValue, f: &mut impl FnMut(&mut SimValue, usize), ); - fn connect_src_regs( + fn connect_to_src_regs( input: impl ToExpr, src_regs: impl ToExpr>, ) { diff --git a/crates/cpu/src/lib.rs b/crates/cpu/src/lib.rs index 2ba775e..ef17595 100644 --- a/crates/cpu/src/lib.rs +++ b/crates/cpu/src/lib.rs @@ -11,5 +11,6 @@ pub mod powerisa_instructions_xml; pub mod reg_alloc; pub mod register; pub mod rename_execute_retire; +pub mod test; pub mod unit; pub mod util; diff --git a/crates/cpu/src/next_pc.rs b/crates/cpu/src/next_pc.rs index b184559..e77a105 100644 --- a/crates/cpu/src/next_pc.rs +++ b/crates/cpu/src/next_pc.rs @@ -106,7 +106,7 @@ pub struct WipDecodedInsn { pub kind: WipDecodedInsnKind, } -#[hdl] +#[hdl(cmp_eq)] pub enum CallStackOp { None, Push(UInt<64>), diff --git a/crates/cpu/src/rename_execute_retire/to_unit_interfaces.rs b/crates/cpu/src/rename_execute_retire/to_unit_interfaces.rs index d3ec39a..0fd362e 100644 --- a/crates/cpu/src/rename_execute_retire/to_unit_interfaces.rs +++ b/crates/cpu/src/rename_execute_retire/to_unit_interfaces.rs @@ -1,11 +1,15 @@ // SPDX-License-Identifier: LGPL-3.0-or-later // See Notices.txt for copyright information -use crate::{config::CpuConfig, rename_execute_retire::ExecuteToUnitInterface}; +use crate::{ + config::{CpuConfig, CpuConfigUnitCount}, + rename_execute_retire::ExecuteToUnitInterface, +}; use fayalite::{ bundle::{BundleField, BundleType, NoBuilder}, expr::ops::FieldAccess, intern::{Intern, Interned, Memoize}, + module::{connect_with_loc, wire_with_loc}, prelude::*, ty::{ OpaqueSimValue, OpaqueSimValueSlice, OpaqueSimValueWriter, OpaqueSimValueWritten, @@ -102,6 +106,42 @@ impl> ExecuteToUnitInterfaces { } MyMemoize(PhantomData).get_owned(this.to_expr()) } + #[track_caller] + pub fn unit_fields_as_array_wire_with_loc( + this: impl ToExpr, + wire_name: &str, + source_location: SourceLocation, + array_wire_is_dest: bool, + ) -> Expr, CpuConfigUnitCount>> { + let this = this.to_expr(); + let config = this.ty().config; + let array_wire = wire_with_loc( + wire_name, + source_location, + ArrayType[ExecuteToUnitInterface[config]][CpuConfigUnitCount[config]], + ); + for (unit_field, array_element) in Self::unit_fields(this).into_iter().zip(array_wire) { + if array_wire_is_dest { + connect_with_loc(array_element, unit_field, source_location); + } else { + connect_with_loc(unit_field, array_element, source_location); + } + } + array_wire + } + #[track_caller] + pub fn unit_fields_as_array_wire( + this: impl ToExpr, + wire_name: &str, + array_wire_is_dest: bool, + ) -> Expr, CpuConfigUnitCount>> { + Self::unit_fields_as_array_wire_with_loc( + this, + wire_name, + SourceLocation::caller(), + array_wire_is_dest, + ) + } } #[doc(hidden)] diff --git a/crates/cpu/src/test.rs b/crates/cpu/src/test.rs new file mode 100644 index 0000000..011c7dd --- /dev/null +++ b/crates/cpu/src/test.rs @@ -0,0 +1,4 @@ +// SPDX-License-Identifier: LGPL-3.0-or-later +// See Notices.txt for copyright information + +pub mod decode_and_run_single_insn; diff --git a/crates/cpu/src/test/decode_and_run_single_insn.rs b/crates/cpu/src/test/decode_and_run_single_insn.rs new file mode 100644 index 0000000..c2accd4 --- /dev/null +++ b/crates/cpu/src/test/decode_and_run_single_insn.rs @@ -0,0 +1,951 @@ +// SPDX-License-Identifier: LGPL-3.0-or-later +// See Notices.txt for copyright information + +use crate::{ + config::{CpuConfig, CpuConfigUnitCount, PhantomConstCpuConfig}, + instruction::{ + COMMON_MOP_SRC_LEN, MOp, MOpDestReg, MOpRegNum, MOpTrait, MoveRegMOp, PRegNum, UnitNum, + UnitOutRegNum, + }, + next_pc::{CallStackOp, FETCH_BLOCK_ID_WIDTH}, + register::PRegValue, + rename_execute_retire::{ + ExecuteToUnitInterface, GlobalState, MOpId, MOpInstance, NextPcPredictorOp, RenamedMOp, + UnitCausedCancel, UnitEnqueue, UnitFinishCauseCancel, UnitInputsReady, + UnitMOpIsNoLongerSpeculative, UnitOutputReady, to_unit_interfaces::ExecuteToUnitInterfaces, + }, + unit::{HdlUnitKind, UnitMOp}, + util::array_vec::ArrayVec, +}; +use fayalite::{ + bundle::BundleType, + int::UIntInRangeType, + intern::{Intern, Interned}, + module::wire_with_loc, + prelude::*, + util::{prefix_sum::reduce, ready_valid::ReadyValid}, +}; + +/// make arrays dynamically-sized to avoid putting large types on the stack +#[hdl(get(|c| 1 << MOpRegNum::WIDTH))] +type MOpRegCount> = DynSize; + +#[hdl(cmp_eq, no_static)] +pub struct Registers> { + pub regs: ArrayType, MOpRegCount>, + pub config: C, +} + +impl Registers { + #[hdl] + pub fn zeroed(self) -> Expr { + #[hdl] + Self { + regs: repeat(PRegValue::zeroed().into_trace_as_string(), self.regs.len()), + config: self.config, + } + } + #[hdl] + pub fn zeroed_sim(self) -> SimValue { + #[hdl(sim)] + Self { + regs: vec![PRegValue::zeroed_sim().into_trace_as_string(); self.regs.len()], + config: self.config, + } + } +} + +#[hdl(no_static)] +pub struct DecodeOneInsnOutput { + pub mops: ArrayVec, MaxMOpCount>, + pub size_in_bytes: UInt<4>, + pub is_illegal: Bool, +} + +pub trait DecodeOneInsn: BundleType { + type Input: Type; + fn input_ty(self) -> Self::Input; + type MaxMOpCount: Size; + fn max_mop_count(self) -> ::SizeType; + fn connect_io( + this: Expr, + input: Expr, + output: Expr>, + ); +} + +pub type DecodeOneInsnInput = ::Input; +#[doc(hidden)] +#[expect(non_upper_case_globals)] +pub const DecodeOneInsnInput: DecodeOneInsnInputWithoutGenerics = + DecodeOneInsnInputWithoutGenerics {}; +#[doc(hidden)] +pub struct DecodeOneInsnInputWithoutGenerics {} + +impl std::ops::Index for DecodeOneInsnInputWithoutGenerics { + type Output = DecodeOneInsnInput; + + fn index(&self, index: T) -> &Self::Output { + Interned::into_inner(index.input_ty().intern_sized()) + } +} + +pub type DecodeOneInsnMaxMOpCount = ::MaxMOpCount; +#[doc(hidden)] +#[expect(non_upper_case_globals)] +pub const DecodeOneInsnMaxMOpCount: DecodeOneInsnMaxMOpCountWithoutGenerics = + DecodeOneInsnMaxMOpCountWithoutGenerics {}; +#[doc(hidden)] +pub struct DecodeOneInsnMaxMOpCountWithoutGenerics {} + +impl std::ops::Index for DecodeOneInsnMaxMOpCountWithoutGenerics { + type Output = ::SizeType; + + fn index(&self, index: T) -> &Self::Output { + Interned::into_inner(index.max_mop_count().intern_sized()) + } +} + +#[hdl(no_static)] +pub struct DecodeAndRunSingleInsnInput, I> { + pub decoder_input: I, + pub fetch_block_id: UInt<{ FETCH_BLOCK_ID_WIDTH }>, + pub first_id: MOpId, + pub pc: UInt<64>, + pub predicted_next_pc: UInt<64>, + pub regs: Registers, + pub config: C, +} + +#[hdl(no_static)] +pub struct DecodeAndRunSingleInsnOutput, MaxMOpCount: Size> { + pub regs: Registers, + pub cancel_and_start_at: HdlOption>, + pub retired_insns: ArrayVec, MaxMOpCount>, + pub config: C, +} + +#[hdl(no_static)] +struct UnrenamedMOpState> { + unrenamed: MOpInstance, + renamed: HdlOption>>, + unit_num: TraceAsString>, +} + +#[hdl(no_static)] +enum Error { + NoUnitsOfKind(HdlUnitKind), + UnexpectedOutputReadyId(MOpId), + UnexpectedFinishCauseCancelId(MOpId), + InconsistentState, +} + +#[hdl(no_static)] +struct CancelState> { + canceling_units: ArrayType>, + config: C, +} + +#[hdl] +enum UnitState { + NotYetEnqueued, + SentInputsReady, + OutputReady, + FinishedAndOrCausedCancel, +} + +#[hdl(no_static)] +struct RunMOpState, MaxMOpCount: Size> { + mop_index: UIntInRangeType, MaxMOpCount>, + unit_state: UnitState, + config: C, +} + +#[hdl(no_static)] +enum RunState, MaxMOpCount: Size> { + RunningMOp(RunMOpState), + CancelingUnits(CancelState), + Finished, + Error(TraceAsString), +} + +#[hdl(no_static)] +struct OutputState> { + dest_value: TraceAsString, + predictor_op: NextPcPredictorOp, +} + +#[hdl(no_static)] +struct DecodeAndRunSingleInsnState, MaxMOpCount: Size> { + mops: ArrayVec, MaxMOpCount>, + regs: Registers, + run_state: RunState, + output_state: HdlOption>, + cancel_and_start_at: HdlOption>, + retired_insns: ArrayVec, MaxMOpCount>, + config: C, +} + +#[hdl(no_static)] +enum StepOutput, MaxMOpCount: Size> { + Finished(DecodeAndRunSingleInsnOutput), + Step(DecodeAndRunSingleInsnState), + Error(TraceAsString), +} + +#[hdl] +fn connect_to_unit_nop>( + to_unit: Expr>, + global_state: impl ToExpr, +) { + #[hdl] + let ExecuteToUnitInterface::<_> { + global_state: to_unit_global_state, + enqueue, + inputs_ready, + is_no_longer_speculative, + cant_cause_cancel: _, + output_ready: _, + finish_cause_cancel: _, + unit_outputs_ready, + cancel_all, + config: _, + } = to_unit; + connect(to_unit_global_state, global_state); + connect(enqueue.data, enqueue.ty().data.HdlNone()); + connect(inputs_ready, inputs_ready.ty().HdlNone()); + connect( + is_no_longer_speculative, + is_no_longer_speculative.ty().HdlNone(), + ); + connect(unit_outputs_ready, false); + connect(cancel_all.data, HdlNone()); +} + +impl DecodeAndRunSingleInsnState { + #[hdl] + fn new( + input: Expr>, + decoder_output: Expr>, + config: C, + max_mop_count: MaxMOpCount::SizeType, + ) -> Expr { + #[hdl] + let new_state = wire(DecodeAndRunSingleInsnState[config][max_mop_count]); + #[hdl] + let Self { + mops, + regs, + run_state, + output_state, + cancel_and_start_at, + retired_insns, + config: _, + } = new_state; + connect(run_state, run_state.ty().Finished()); + connect(output_state, output_state.ty().HdlNone()); + connect(cancel_and_start_at, HdlNone()); + connect(retired_insns, retired_insns.ty().new()); + connect( + mops, + ArrayVec::map( + decoder_output.mops, + mops.ty().element(), + |index, decoded_mop| { + if index == 0 { + connect( + run_state, + run_state.ty().RunningMOp( + #[hdl] + RunMOpState::<_, _> { + mop_index: 0usize.cast_to(run_state.ty().RunningMOp.mop_index), + unit_state: UnitState.NotYetEnqueued(), + config, + }, + ), + ); + } + let retval = wire_with_loc( + &format!("mops_{index}"), + SourceLocation::caller(), + UnrenamedMOpState[config], + ); + #[hdl] + let UnrenamedMOpState::<_> { + unrenamed, + renamed, + unit_num, + } = retval; + #[hdl] + let MOpInstance::<_> { + fetch_block_id, + id, + pc, + predicted_next_pc, + size_in_bytes, + is_first_mop_in_insn, + is_last_mop_in_insn, + mop, + } = unrenamed; + connect(fetch_block_id, input.fetch_block_id); + connect(id, (input.first_id + index).cast_to_static::()); + connect(pc, input.pc); + connect(predicted_next_pc, input.predicted_next_pc); + connect(size_in_bytes, decoder_output.size_in_bytes); + connect(is_first_mop_in_insn, index == 0); + connect( + is_last_mop_in_insn, + ArrayVec::len(decoder_output.mops).cmp_eq(index + 1), + ); + connect(mop, decoded_mop); + #[hdl] + let renamed_untransformed_move = wire( + HdlOption[TraceAsString[UnitMOp[PRegNum[config]][PRegNum[config]] + [MoveRegMOp[PRegNum[config]][PRegNum[config]]]]], + ); + #[hdl] + if let MOp::TransformedMove(_) = *mop { + connect( + renamed_untransformed_move, + renamed_untransformed_move.ty().HdlNone(), + ); + } else { + let unit_kind = MOp::kind(*mop); + let available_units = config.get().available_units_for_kind(unit_kind); + let chosen_unit = reduce( + available_units.into_iter().enumerate().map( + |(unit_index, available_unit)| { + #[hdl] + let chosen_unit = wire(UnitNum[config]); + connect(chosen_unit, chosen_unit.ty().const_zero()); + #[hdl] + if available_unit { + connect( + chosen_unit, + chosen_unit.ty().from_index(unit_index), + ); + } + chosen_unit + }, + ), + |a, b| { + #[hdl] + let chosen_unit = wire(UnitNum[config]); + connect(chosen_unit, a); + #[hdl] + if a.cmp_eq(chosen_unit.ty().const_zero()) { + connect(chosen_unit, b); + } + chosen_unit + }, + ) + .unwrap_or(UnitNum[config].const_zero()); + #[hdl] + if chosen_unit.cmp_eq(chosen_unit.ty().const_zero()) { + connect( + run_state, + run_state + .ty() + .Error(Error.NoUnitsOfKind(unit_kind).to_trace_as_string()), + ); + } + let unit_out_reg_num_ty = UnitOutRegNum[config]; + connect( + renamed_untransformed_move, + HdlSome( + MOpTrait::map_regs( + *mop, + #[hdl] + PRegNum::<_> { + unit_num: chosen_unit, + unit_out_reg: #[hdl] + UnitOutRegNum::<_> { + value: !unit_out_reg_num_ty.value.zero(), + config, + }, + }, + PRegNum[config], + &mut |src_reg, index| { + #[hdl] + let renamed_src_reg = wire(PRegNum[config]); + #[hdl] + if src_reg.cmp_eq(MOpRegNum::const_zero()) { + connect( + renamed_src_reg, + renamed_src_reg.ty().const_zero(), + ); + } else { + connect( + renamed_src_reg, + #[hdl] + PRegNum::<_> { + unit_num: chosen_unit, + unit_out_reg: unit_out_reg_num_ty + .new_sim(index), + }, + ); + } + renamed_src_reg + }, + ) + .to_trace_as_string(), + ), + ); + } + connect(renamed, renamed.ty().HdlNone()); + connect(*unit_num, unit_num.ty().inner_ty().const_zero()); + #[hdl] + if let HdlSome(renamed_untransformed_move) = renamed_untransformed_move { + let v = UnitMOp::try_with_transformed_move_op( + *renamed_untransformed_move, + renamed.ty().HdlSome.inner_ty().TransformedMove, + |dest, _src| { + connect(dest, dest.ty().HdlNone()); + }, + ); + #[hdl] + if let HdlSome(v) = v { + connect(renamed, HdlSome(v.to_trace_as_string())); + connect(*unit_num, MOpTrait::dest_reg(v).unit_num); + } + } + retval + }, + ), + ); + connect(regs, input.regs); + #[hdl] + if PRegValue::zeroed().cmp_ne(*regs.regs[MOpRegNum::CONST_ZERO_REG_NUM as usize]) { + connect( + run_state, + run_state + .ty() + .Error(Error.InconsistentState().to_trace_as_string()), + ); + } + new_state + } + #[hdl] + fn step( + this: Expr, + to_units: Expr>, + global_state: Expr, + ) -> Expr> { + #[hdl] + let Self { + mops, + regs, + run_state, + output_state, + cancel_and_start_at, + retired_insns, + config, + } = this; + let config = config.ty(); + let max_mop_count = MaxMOpCount::from_usize(mops.ty().capacity()); + #[hdl] + let stepped = wire(StepOutput[config][max_mop_count]); + let to_units_as_array = ExecuteToUnitInterfaces::unit_fields_as_array_wire( + to_units, + "to_units_as_array", + false, + ); + for to_unit in to_units_as_array { + connect_to_unit_nop(to_unit, global_state); + } + #[hdl] + let stepped_step = wire(stepped.ty().Step); + connect(stepped_step, this); + connect(stepped, stepped.ty().Step(stepped_step)); + #[hdl] + match run_state { + RunState::<_, _>::RunningMOp(run_mop_state) => { + #[hdl] + let RunMOpState::<_, _> { + mop_index, + unit_state, + config: _, + } = run_mop_state; + let mop_index = mop_index.cast_to(UInt[mop_index.ty().bit_width()]); + #[hdl] + let mop = wire(mops.ty().element()); + connect(mop, mops[mop_index]); + #[hdl] + let UnrenamedMOpState::<_> { + unrenamed, + renamed, + unit_num, + } = mop; + #[hdl] + let unrenamed_src_regs = wire(); + connect( + unrenamed_src_regs, + repeat( + MOpRegNum::const_zero(), + ConstUsize::<{ COMMON_MOP_SRC_LEN }>, + ), + ); + MOpTrait::connect_to_src_regs(*unrenamed.mop, unrenamed_src_regs); + #[hdl] + let src_values: Array< + TraceAsString, + { COMMON_MOP_SRC_LEN }, + > = wire(); + for (src_value, src_reg) in src_values.into_iter().zip(unrenamed_src_regs) { + connect(src_value, regs.regs[src_reg.value]); + } + #[hdl] + if let HdlSome(unit_index) = UnitNum::as_index(*unit_num) { + #[hdl] + let to_unit = wire(to_units_as_array.ty().element()); + connect(to_units_as_array[unit_index], to_unit); + connect_to_unit_nop(to_unit, global_state); + #[hdl] + let ExecuteToUnitInterface::<_> { + global_state: _, + enqueue, + inputs_ready, + is_no_longer_speculative, + cant_cause_cancel: _, // we don't track if it can cause a cancel + output_ready, + finish_cause_cancel, + unit_outputs_ready, + cancel_all, + config: _, + } = to_unit; + connect(unit_outputs_ready, true); + connect(cancel_all.data, HdlNone()); + #[hdl] + let unit_state_after_start = wire(); + connect(unit_state_after_start, unit_state); + #[hdl] + if let UnitState::NotYetEnqueued = unit_state { + #[hdl] + if let HdlSome(renamed) = renamed { + let mop = #[hdl] + MOpInstance::<_> { + fetch_block_id: unrenamed.fetch_block_id, + id: unrenamed.id, + pc: unrenamed.pc, + predicted_next_pc: unrenamed.predicted_next_pc, + size_in_bytes: unrenamed.size_in_bytes, + is_first_mop_in_insn: unrenamed.is_first_mop_in_insn, + is_last_mop_in_insn: unrenamed.is_last_mop_in_insn, + mop: renamed, + }; + connect( + enqueue.data, + HdlSome( + #[hdl] + UnitEnqueue::<_> { mop, config }, + ), + ); + #[hdl] + if enqueue.ready { + connect( + inputs_ready, + HdlSome( + #[hdl] + UnitInputsReady::<_> { + mop, + src_values, + config, + }, + ), + ); + connect( + is_no_longer_speculative, + HdlSome( + #[hdl] + UnitMOpIsNoLongerSpeculative::<_> { + id: unrenamed.id, + config, + }, + ), + ); + connect(unit_state_after_start, UnitState.SentInputsReady()); + } + } else { + connect( + stepped, + stepped + .ty() + .Error(Error.InconsistentState().to_trace_as_string()), + ); + } + } + #[hdl] + let unit_state_after_output_ready = wire(); + connect(unit_state_after_output_ready, unit_state_after_start); + #[hdl] + let output_state_after_output_ready = wire(output_state.ty()); + connect(output_state_after_output_ready, output_state); + #[hdl] + if let HdlSome(output_ready) = output_ready { + #[hdl] + let UnitOutputReady::<_> { + id: output_ready_id, + dest_value, + predictor_op, + } = output_ready; + #[hdl] + match unit_state_after_start { + UnitState::SentInputsReady => { + connect( + output_state_after_output_ready, + HdlSome( + #[hdl] + OutputState::<_> { + dest_value, + predictor_op, + }, + ), + ); + connect(unit_state_after_output_ready, UnitState.OutputReady()); + } + UnitState::NotYetEnqueued + | UnitState::OutputReady + | UnitState::FinishedAndOrCausedCancel => connect( + stepped, + stepped + .ty() + .Error(Error.InconsistentState().to_trace_as_string()), + ), + } + #[hdl] + if unrenamed.id.cmp_ne(output_ready_id) { + connect( + stepped, + stepped.ty().Error( + Error + .UnexpectedOutputReadyId(output_ready_id) + .to_trace_as_string(), + ), + ); + } + } + #[hdl] + if let HdlSome(finish_cause_cancel) = finish_cause_cancel { + #[hdl] + let UnitFinishCauseCancel::<_> { + id: finish_cause_cancel_id, + caused_cancel, + config: _, + } = finish_cause_cancel; + connect(stepped_step.output_state, output_state.ty().HdlNone()); + #[hdl] + match unit_state_after_output_ready { + UnitState::OutputReady => {} + UnitState::NotYetEnqueued + | UnitState::SentInputsReady + | UnitState::FinishedAndOrCausedCancel => connect( + stepped, + stepped + .ty() + .Error(Error.InconsistentState().to_trace_as_string()), + ), + } + #[hdl] + let do_retire = wire(); + #[hdl] + if do_retire { + #[hdl] + if let HdlSome(output_state) = output_state_after_output_ready { + #[hdl] + let OutputState::<_> { + dest_value, + predictor_op, + } = output_state; + let old_len = ArrayVec::len(retired_insns); + let len_ty = old_len.ty(); + let old_len = old_len.cast_to(UInt[len_ty.bit_width()]); + connect( + ArrayVec::len(stepped_step.retired_insns), + (old_len + 1u8).cast_to(len_ty), + ); + connect(stepped_step.retired_insns[old_len], predictor_op); + for dest_reg in MOpDestReg::regs(MOpTrait::dest_reg(*unrenamed.mop)) + { + #[hdl] + if MOpRegNum::const_zero().cmp_ne(dest_reg) { + connect(stepped_step.regs.regs[dest_reg.value], dest_value); + } + } + } else { + connect( + stepped, + stepped + .ty() + .Error(Error.InconsistentState().to_trace_as_string()), + ); + } + } + #[hdl] + if let HdlSome(caused_cancel) = caused_cancel { + #[hdl] + let UnitCausedCancel::<_> { + start_at_pc, + cancel_after_retire, + config: _, + } = caused_cancel; + connect(stepped_step.cancel_and_start_at, HdlSome(start_at_pc)); + connect(do_retire, cancel_after_retire); + connect( + stepped_step.run_state, + stepped_step.ty().run_state.CancelingUnits( + #[hdl] + CancelState::<_> { + canceling_units: repeat( + true, + CancelState[config].canceling_units.len(), + ), + config, + }, + ), + ); + } else { + connect(do_retire, true); + #[hdl] + let next_mop_index = wire(mops.ty().len_ty()); + connect( + next_mop_index, + (mop_index + 1u8).cast_to(next_mop_index.ty()), + ); + #[hdl] + if next_mop_index.cmp_lt(ArrayVec::len(mops)) { + connect( + stepped_step.run_state, + stepped_step.ty().run_state.RunningMOp( + #[hdl] + RunMOpState::<_, _> { + mop_index: next_mop_index + .cast_to(mop_index.ty()) + .cast_to(run_mop_state.ty().mop_index), + unit_state: UnitState.NotYetEnqueued(), + config, + }, + ), + ); + } else { + connect( + stepped_step.run_state, + stepped_step.ty().run_state.Finished(), + ); + } + } + #[hdl] + if unrenamed.id.cmp_ne(finish_cause_cancel_id) { + connect( + stepped, + stepped.ty().Error( + Error + .UnexpectedFinishCauseCancelId(finish_cause_cancel_id) + .to_trace_as_string(), + ), + ); + } + } else { + connect(stepped_step.output_state, output_state_after_output_ready); + connect( + stepped_step.run_state, + stepped_step.ty().run_state.RunningMOp( + #[hdl] + RunMOpState::<_, _> { + mop_index: run_mop_state.mop_index, + unit_state: unit_state_after_output_ready, + config, + }, + ), + ); + } + } else { + #[hdl] + if let MOp::TransformedMove(mop) = *unrenamed.mop { + #[hdl] + let MoveRegMOp::<_, _> { common: _ } = mop; + } else { + connect( + stepped, + stepped + .ty() + .Error(Error.InconsistentState().to_trace_as_string()), + ); + } + let old_len = ArrayVec::len(retired_insns); + let len_ty = old_len.ty(); + let old_len = old_len.cast_to(UInt[len_ty.bit_width()]); + connect( + ArrayVec::len(stepped_step.retired_insns), + (old_len + 1u8).cast_to(len_ty), + ); + connect( + stepped_step.retired_insns[old_len], + #[hdl] + NextPcPredictorOp::<_> { + call_stack_op: CallStackOp.None(), + cond_br_taken: HdlNone(), + config, + }, + ); + for dest_reg in MOpDestReg::regs(MOpTrait::dest_reg(*unrenamed.mop)) { + #[hdl] + if MOpRegNum::const_zero().cmp_ne(dest_reg) { + connect(stepped_step.regs.regs[dest_reg.value], src_values[0]); + } + } + } + } + RunState::<_, _>::CancelingUnits(cancel_state) => { + #[hdl] + let CancelState::<_> { + canceling_units, + config: _, + } = cancel_state; + #[hdl] + let done_canceling_units = wire(); + connect(done_canceling_units, true); + #[hdl] + let still_canceling_units = wire(canceling_units.ty()); + for ((to_unit, canceling_unit), still_canceling_unit) in to_units_as_array + .into_iter() + .zip(canceling_units) + .zip(still_canceling_units) + { + connect(still_canceling_unit, false); + #[hdl] + if canceling_unit { + connect(to_unit.cancel_all.data, HdlSome(())); + #[hdl] + if !to_unit.cancel_all.ready { + connect(still_canceling_unit, true); + connect(done_canceling_units, false); + } + } + } + #[hdl] + if done_canceling_units { + connect( + stepped, + stepped.ty().Finished( + #[hdl] + DecodeAndRunSingleInsnOutput::<_, _> { + regs, + cancel_and_start_at, + retired_insns, + config, + }, + ), + ); + } else { + connect( + stepped_step.run_state, + run_state.ty().CancelingUnits( + #[hdl] + CancelState::<_> { + canceling_units: still_canceling_units, + config, + }, + ), + ); + } + } + RunState::<_, _>::Finished => connect( + stepped, + stepped.ty().Finished( + #[hdl] + DecodeAndRunSingleInsnOutput::<_, _> { + regs, + cancel_and_start_at, + retired_insns, + config, + }, + ), + ), + RunState::<_, _>::Error(error) => connect(stepped, stepped.ty().Error(error)), + } + stepped + } +} + +#[hdl_module] +pub fn decode_and_run_single_insn( + config: C, + decoder: Interned>, +) { + #[hdl] + let cd: ClockDomain = m.input(); + #[hdl] + let input: ReadyValid>> = m.input( + ReadyValid[DecodeAndRunSingleInsnInput[config][DecodeOneInsnInput[decoder.io_ty()]]], + ); + #[hdl] + let global_state: GlobalState = m.input(); + #[hdl] + let output: ReadyValid>> = m + .output( + ReadyValid + [DecodeAndRunSingleInsnOutput[config][DecodeOneInsnMaxMOpCount[decoder.io_ty()]]], + ); + #[hdl] + let to_units: ExecuteToUnitInterfaces = m.output(ExecuteToUnitInterfaces[config]); + #[hdl] + let error: Bool = m.output(); + + connect(error, false); + + #[hdl] + let decoder = instance(decoder); + #[hdl] + let decoder_input = wire(decoder.ty().input_ty()); + connect(decoder_input, decoder_input.ty().uninit()); + #[hdl] + let decoder_output = wire(DecodeOneInsnOutput[decoder.ty().max_mop_count()]); + D::connect_io(decoder, decoder_input, decoder_output); + + #[hdl] + let state_reg = reg_builder().clock_domain(cd).reset( + HdlOption[DecodeAndRunSingleInsnState[config][decoder.ty().max_mop_count()]].HdlNone(), + ); + + #[hdl] + if let HdlSome(state) = state_reg { + connect(input.ready, false); + let step = DecodeAndRunSingleInsnState::step(state, to_units, global_state); + #[hdl] + match step { + StepOutput::<_, _>::Finished(v) => { + connect(output.data, HdlSome(v)); + #[hdl] + if output.ready { + connect(state_reg, state_reg.ty().HdlNone()); + } + } + StepOutput::<_, _>::Step(state) => { + connect(state_reg, HdlSome(state)); + connect(output.data, output.ty().data.HdlNone()); + } + StepOutput::<_, _>::Error(_) => { + connect(output.data, output.ty().data.HdlNone()); + connect(error, true); + } + } + } else { + for to_unit in ExecuteToUnitInterfaces::unit_fields(to_units) { + connect_to_unit_nop(to_unit, global_state); + } + connect(input.ready, true); + connect(output.data, output.ty().data.HdlNone()); + #[hdl] + if let HdlSome(input) = input.data { + connect( + state_reg, + HdlSome(DecodeAndRunSingleInsnState::new( + input, + decoder_output, + config, + decoder.ty().max_mop_count(), + )), + ); + } + } +} diff --git a/crates/cpu/tests/units_formal.rs b/crates/cpu/tests/units_formal.rs new file mode 100644 index 0000000..e84103c --- /dev/null +++ b/crates/cpu/tests/units_formal.rs @@ -0,0 +1,224 @@ +// SPDX-License-Identifier: LGPL-3.0-or-later +// See Notices.txt for copyright information + +use cpu::{ + config::{CpuConfig, UnitConfig}, + decoder::simple_power_isa, + instruction::MOpRegNum, + next_pc::CallStackOp, + register::{FlagsMode, PRegFlags, PRegFlagsPowerISA, PRegFlagsPowerISAView, PRegValue}, + rename_execute_retire::{ + GlobalState, NextPcPredictorOp, to_unit_interfaces::ExecuteToUnitInterfaces, + }, + test::decode_and_run_single_insn::{ + DecodeAndRunSingleInsnInput, DecodeAndRunSingleInsnOutput, DecodeOneInsnInput, + DecodeOneInsnMaxMOpCount, decode_and_run_single_insn, + }, + unit::{UnitKind, UnitTrait}, + util::array_vec::ArrayVec, +}; +use fayalite::{ + firrtl::ExportOptions, + module::{instance_with_loc, transform::simplify_enums::SimplifyEnumsKind}, + prelude::*, + ty::StaticType, +}; +use std::num::NonZero; + +#[hdl_module] +fn formal_harness(config: PhantomConst) { + #[hdl] + let cd: ClockDomain = m.output(); + connect(cd.clk, fayalite::formal::formal_global_clock()); + connect(cd.rst, fayalite::formal::formal_reset().to_reset()); + + #[hdl] + let input: DecodeAndRunSingleInsnInput< + PhantomConst, + DecodeOneInsnInput, + > = m.input(DecodeAndRunSingleInsnInput[config][StaticType::TYPE]); + + #[hdl] + let output: HdlOption< + DecodeAndRunSingleInsnOutput< + PhantomConst, + DecodeOneInsnMaxMOpCount, + >, + > = m.output(HdlOption[DecodeAndRunSingleInsnOutput[config][ConstUsize]]); + + #[hdl] + let decode_and_run = instance(decode_and_run_single_insn( + config, + simple_power_isa::decode_one_insn(), + )); + connect(decode_and_run.cd, cd); + #[hdl] + let need_to_send_input_reg = reg_builder().clock_domain(cd).reset(true); + #[hdl] + if need_to_send_input_reg { + connect(decode_and_run.input.data, HdlSome(input)); + #[hdl] + if decode_and_run.input.ready { + connect(need_to_send_input_reg, false); + } + } else { + connect( + decode_and_run.input.data, + decode_and_run.ty().input.data.HdlNone(), + ); + } + connect( + decode_and_run.global_state, + #[hdl] + GlobalState { + flags_mode: FlagsMode.PowerISA( + #[hdl] + PRegFlagsPowerISA {}, + ), + }, + ); + connect(decode_and_run.output.ready, true); + connect(output, decode_and_run.output.data); + for (unit_index, unit) in config.get().units.iter().enumerate() { + let dyn_unit = unit.kind.unit(config, unit_index); + let unit = instance_with_loc( + &decode_and_run.ty().to_units.unit_field_name(unit_index), + dyn_unit.module(), + SourceLocation::caller(), + ); + connect( + dyn_unit.from_execute(unit), + ExecuteToUnitInterfaces::unit_fields(decode_and_run.to_units)[unit_index], + ); + if let Some(unit_cd) = dyn_unit.cd(unit) { + connect(unit_cd, cd); + } + } + hdl_assert(cd.clk, !decode_and_run.error, ""); +} + +#[hdl_module] +fn check_power_isa_add_formal(config: PhantomConst) { + #[hdl] + let harness = instance(formal_harness(config)); + let cd = harness.cd; + #[hdl] + let DecodeAndRunSingleInsnInput::<_, _> { + decoder_input, + fetch_block_id, + first_id, + pc, + predicted_next_pc, + regs: input_regs, + config: _, + } = harness.input; + // add r3, r3, r4 + connect(decoder_input, (0x7c632214_u32, HdlNone())); + connect(fetch_block_id, 0u8); + connect(first_id, 0u16); + connect(pc, 0x1000_u64); + connect(predicted_next_pc, 0x1004_u64); + connect( + input_regs.regs, + repeat( + PRegValue::zeroed().to_trace_as_string(), + 1 << MOpRegNum::WIDTH, + ), + ); + #[hdl] + let input_r3 = wire(); + connect(input_r3, any_const(StaticType::TYPE)); + #[hdl] + let input_r4 = wire(); + connect(input_r4, any_const(StaticType::TYPE)); + connect( + input_regs.regs[MOpRegNum::power_isa_gpr_reg_imm(3).value].int_fp, + input_r3, + ); + connect( + input_regs.regs[MOpRegNum::power_isa_gpr_reg_imm(4).value].int_fp, + input_r4, + ); + #[hdl] + if let HdlSome(output) = harness.output { + #[hdl] + let DecodeAndRunSingleInsnOutput::<_, _> { + regs, + cancel_and_start_at, + retired_insns, + config: _, + } = output; + hdl_assert(cd.clk, cancel_and_start_at.cmp_eq(HdlNone()), ""); + hdl_assert(cd.clk, ArrayVec::len(retired_insns).cmp_eq(1u8), ""); + #[hdl] + let NextPcPredictorOp::<_> { + call_stack_op, + cond_br_taken, + config: _, + } = retired_insns[0]; + hdl_assert(cd.clk, call_stack_op.cmp_eq(CallStackOp.None()), ""); + hdl_assert(cd.clk, cond_br_taken.cmp_eq(HdlNone()), ""); + #[hdl] + let expected_regs = wire(regs.ty()); + for (reg_index, expected) in expected_regs.regs.into_iter().enumerate() { + let reg_num = reg_index as u32; + if reg_num == MOpRegNum::power_isa_gpr_reg_num(3) { + connect(expected.int_fp, (input_r3 + input_r4).cast_to_static()); + let PRegFlagsPowerISAView { + unused: _, + xer_ca, + xer_ca32, + xer_ov, + xer_ov32, + cr_lt, + cr_gt, + cr_eq, + so, + .. + } = PRegFlags::view::(expected.flags); + let input_r3_s = input_r3.cast_to_static::>(); + let input_r4_s = input_r4.cast_to_static::>(); + let u64_sum = input_r3 + input_r4; + let s64_sum = input_r3_s + input_r4_s; + let u32_sum = input_r3.cast_to(UInt[32]) + input_r4.cast_to(UInt[32]); + let s32_sum = input_r3.cast_to(SInt[32]) + input_r4.cast_to(SInt[32]); + let sum_as_s64 = u64_sum.cast_to(SInt[64]); + connect(xer_ca, u64_sum[64]); + connect(xer_ca32, u32_sum[32]); + connect(xer_ov, s64_sum.cmp_lt(i64::MIN) | s64_sum.cmp_gt(i64::MAX)); + connect( + xer_ov32, + s32_sum.cmp_lt(i32::MIN) | s32_sum.cmp_gt(i32::MAX), + ); + connect(cr_gt, sum_as_s64.cmp_gt(0i64)); + connect(cr_lt, sum_as_s64.cmp_lt(0i64)); + connect(cr_eq, sum_as_s64.cmp_eq(0i64)); + connect(so, xer_ov); // TODO: also propagate from input SO + } else { + connect(expected, input_regs.regs[reg_index]); + } + } + hdl_assert(cd.clk, expected_regs.cmp_eq(regs), ""); + } +} + +#[test] +fn test_power_isa_add_formal() { + let config = PhantomConst::new_sized(CpuConfig::new( + vec![UnitConfig::new(UnitKind::AluBranch)], + NonZero::new(20).unwrap(), + )); + let dut = check_power_isa_add_formal(config); + println!("starting assert formal"); + assert_formal( + "test_power_isa_add_formal", + dut, + FormalMode::Prove, + 10, + None, + ExportOptions { + simplify_enums: Some(SimplifyEnumsKind::ReplaceWithBundleOfUInts), + ..Default::default() + }, + ); +}