WIP: add test_power_isa_add_sim
All checks were successful
/ test (pull_request) Successful in 1h35m6s

This commit is contained in:
Jacob Lifshay 2026-06-05 01:37:27 -07:00
parent 1bc59716c5
commit 9cc556c988
Signed by: programmerjake
SSH key fingerprint: SHA256:HnFTLGpSm4Q4Fj502oCFisjZSoakwEuTsJJMSke63RQ
3 changed files with 28344 additions and 8 deletions

View file

@ -937,6 +937,7 @@ pub fn decode_and_run_single_insn<C: Type + PhantomConstCpuConfig, D: Type + Dec
connect(output.data, output.ty().data.HdlNone()); connect(output.data, output.ty().data.HdlNone());
#[hdl] #[hdl]
if let HdlSome(input) = input.data { if let HdlSome(input) = input.data {
connect(decoder_input, input.decoder_input);
connect( connect(
state_reg, state_reg,
HdlSome(DecodeAndRunSingleInsnState::new( HdlSome(DecodeAndRunSingleInsnState::new(

File diff suppressed because it is too large Load diff

View file

@ -95,17 +95,34 @@ fn formal_harness(config: PhantomConst<CpuConfig>) {
hdl_assert(cd.clk, !decode_and_run.error, ""); hdl_assert(cd.clk, !decode_and_run.error, "");
} }
#[derive(Copy, Clone)]
struct R3R4AnyConst {
r3_any_const: Expr<UInt<64>>,
r4_any_const: Expr<UInt<64>>,
}
impl R3R4AnyConst {
#[track_caller]
fn new() -> Self {
Self {
r3_any_const: any_const(StaticType::TYPE),
r4_any_const: any_const(StaticType::TYPE),
}
}
}
#[hdl_module] #[hdl_module]
fn check_power_isa_add_formal(config: PhantomConst<CpuConfig>) { fn check_power_isa_add_formal(
#[hdl] config: PhantomConst<CpuConfig>,
let clk: Clock = m.input(); r3_r4_any_const: Option<R3R4AnyConst>,
) {
#[hdl] #[hdl]
let cd = wire(); let cd = wire();
connect( connect(
cd, cd,
#[hdl] #[hdl]
ClockDomain { ClockDomain {
clk, clk: formal_global_clock(),
rst: formal_reset().to_reset(), rst: formal_reset().to_reset(),
}, },
); );
@ -113,6 +130,11 @@ fn check_power_isa_add_formal(config: PhantomConst<CpuConfig>) {
let harness = instance(formal_harness(config)); let harness = instance(formal_harness(config));
connect(harness.cd, cd); connect(harness.cd, cd);
#[hdl] #[hdl]
let ran: Bool = m.output();
#[hdl]
let ran_reg = reg_builder().clock_domain(cd).reset(false);
connect(ran, ran_reg);
#[hdl]
let DecodeAndRunSingleInsnInput::<_, _> { let DecodeAndRunSingleInsnInput::<_, _> {
decoder_input, decoder_input,
fetch_block_id, fetch_block_id,
@ -135,12 +157,16 @@ fn check_power_isa_add_formal(config: PhantomConst<CpuConfig>) {
1 << MOpRegNum::WIDTH, 1 << MOpRegNum::WIDTH,
), ),
); );
let R3R4AnyConst {
r3_any_const,
r4_any_const,
} = r3_r4_any_const.unwrap_or_else(|| R3R4AnyConst::new());
#[hdl] #[hdl]
let input_r3 = wire(); let input_r3 = wire();
connect(input_r3, any_const(StaticType::TYPE)); connect(input_r3, r3_any_const);
#[hdl] #[hdl]
let input_r4 = wire(); let input_r4 = wire();
connect(input_r4, any_const(StaticType::TYPE)); connect(input_r4, r4_any_const);
connect( connect(
input_regs.regs[MOpRegNum::power_isa_gpr_reg_imm(3).value].int_fp, input_regs.regs[MOpRegNum::power_isa_gpr_reg_imm(3).value].int_fp,
input_r3, input_r3,
@ -151,6 +177,7 @@ fn check_power_isa_add_formal(config: PhantomConst<CpuConfig>) {
); );
#[hdl] #[hdl]
if let HdlSome(output) = harness.output { if let HdlSome(output) = harness.output {
connect(ran_reg, true);
#[hdl] #[hdl]
let DecodeAndRunSingleInsnOutput::<_, _> { let DecodeAndRunSingleInsnOutput::<_, _> {
regs, regs,
@ -218,8 +245,7 @@ fn test_power_isa_add_formal() {
vec![UnitConfig::new(UnitKind::AluBranch)], vec![UnitConfig::new(UnitKind::AluBranch)],
NonZero::new(20).unwrap(), NonZero::new(20).unwrap(),
)); ));
let m = check_power_isa_add_formal(config); let m = check_power_isa_add_formal(config, None);
println!("starting assert formal");
assert_formal( assert_formal(
"test_power_isa_add_formal", "test_power_isa_add_formal",
m, m,
@ -232,3 +258,34 @@ fn test_power_isa_add_formal() {
}, },
); );
} }
#[hdl]
#[test]
fn test_power_isa_add_sim() {
let config = PhantomConst::new_sized(CpuConfig::new(
vec![UnitConfig::new(UnitKind::AluBranch)],
NonZero::new(20).unwrap(),
));
let r3_r4_any_const = R3R4AnyConst::new();
let m = check_power_isa_add_formal(config, Some(r3_r4_any_const));
let mut sim = Simulation::new(m);
let _checked_vcd_output = cpu::checked_vcd_output!(
&mut sim,
"tests/expected/units_formal_power_isa_add_sim.vcd",
);
sim.write(r3_r4_any_const.r3_any_const, 0x1234u64);
sim.write(r3_r4_any_const.r4_any_const, 0x2345u64);
let clk = formal_global_clock();
let rst = formal_reset();
sim.write_clock(clk, false);
sim.write_reset(rst, true);
for cycle in 0..10 {
sim.advance_time(SimDuration::from_nanos(500));
println!("clock tick: {cycle}");
sim.write_clock(clk, true);
sim.advance_time(SimDuration::from_nanos(500));
sim.write_clock(clk, false);
sim.write_reset(rst, false);
}
assert!(sim.read_bool(sim.io().ran));
}