libre-chip/cpu
3
0
Fork 2
Code Issues 1 Pull requests 1 Projects Releases Packages Wiki Activity Actions

tests/units_formal::test_power_isa_add_formal: formal proof actually starts, though it fails BMC
Some checks failed
/ test (pull_request) Failing after 2h58m41s
Details

Browse source
This commit is contained in:
Jacob Lifshay 2026-06-02 01:38:06 -07:00
parent 14df664277
commit 241255e12c
Signed by: programmerjake
SSH key fingerprint: SHA256:HnFTLGpSm4Q4Fj502oCFisjZSoakwEuTsJJMSke63RQ
1 changed files with 16 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

22
crates/cpu/tests/units_formal.rs
View file

@ -28,9 +28,7 @@ use std::num::NonZero;
#[hdl_module] #[hdl_module]
fn formal_harness(config: PhantomConst<CpuConfig>) { fn formal_harness(config: PhantomConst<CpuConfig>) {
#[hdl] #[hdl]
let cd: ClockDomain = m.output(); let cd: ClockDomain = m.input();
connect(cd.clk, fayalite::formal::formal_global_clock());
connect(cd.rst, fayalite::formal::formal_reset().to_reset());
#[hdl] #[hdl]
let input: DecodeAndRunSingleInsnInput< let input: DecodeAndRunSingleInsnInput<
@ -99,9 +97,21 @@ fn formal_harness(config: PhantomConst<CpuConfig>) {
#[hdl_module] #[hdl_module]
fn check_power_isa_add_formal(config: PhantomConst<CpuConfig>) { fn check_power_isa_add_formal(config: PhantomConst<CpuConfig>) {
#[hdl]
let clk: Clock = m.input();
#[hdl]
let cd = wire();
connect(
cd,
#[hdl]
ClockDomain {
clk,
rst: formal_reset().to_reset(),
},
);
#[hdl] #[hdl]
let harness = instance(formal_harness(config)); let harness = instance(formal_harness(config));
let cd = harness.cd; connect(harness.cd, cd);
#[hdl] #[hdl]
let DecodeAndRunSingleInsnInput::<_, _> { let DecodeAndRunSingleInsnInput::<_, _> {
decoder_input, decoder_input,
@ -208,11 +218,11 @@ 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 dut = check_power_isa_add_formal(config); let m = check_power_isa_add_formal(config);
println!("starting assert formal"); println!("starting assert formal");
assert_formal( assert_formal(
"test_power_isa_add_formal", "test_power_isa_add_formal",
dut, m,
FormalMode::Prove, FormalMode::Prove,
10, 10,
None, None,