programmerjake/cpu
1
0
Fork 0
forked from libre-chip/cpu
Code Pull requests Activity

Compare commits

base: programmerjake:9cc556c9886959d80ac84ad5f0a7234edfc99fa7
Branches Tags
programmerjake:master
programmerjake:decode-and-test-harness
libre-chip:master
libre-chip:wip-splitting-reg-alloc
...
compare: programmerjake:241255e12cb85d8ae7ffc4a929d2b6b9ac5b00ed
Branches Tags
programmerjake:decode-and-test-harness
programmerjake:master
libre-chip:master
libre-chip:wip-splitting-reg-alloc

2 commits
9cc556c988 ... 241255e12c

Author SHA1 Message Date
Jacob Lifshay
241255e12c
tests/units_formal::test_power_isa_add_formal: formal proof actually starts, though it fails BMC 2026-06-02 01:38:06 -07:00
Jacob Lifshay
14df664277
update fayalite 2026-06-02 01:36:12 -07:00
2 changed files with 20 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

8
Cargo.lock generated
View file

@ -388,7 +388,7 @@ checksum = "e8c02a5121d4ea3eb16a80748c74f5549a5665e4c21333c6098f283870fbdea6"
[[package]]
name = "fayalite"
version = "0.3.0"
source = "git+https://git.libre-chip.org/libre-chip/fayalite.git?branch=master#cf3e6cfc6bc33eebf2d2862c7a1948b9cf40ecac"
source = "git+https://git.libre-chip.org/libre-chip/fayalite.git?branch=master#31353862ceba3d255fd6712813a457688b269358"
dependencies = [
"base64",
"bitvec",
@ -417,7 +417,7 @@ dependencies = [
[[package]]
name = "fayalite-proc-macros"
version = "0.3.0"
source = "git+https://git.libre-chip.org/libre-chip/fayalite.git?branch=master#cf3e6cfc6bc33eebf2d2862c7a1948b9cf40ecac"
source = "git+https://git.libre-chip.org/libre-chip/fayalite.git?branch=master#31353862ceba3d255fd6712813a457688b269358"
dependencies = [
"fayalite-proc-macros-impl",
]
@ -425,7 +425,7 @@ dependencies = [
[[package]]
name = "fayalite-proc-macros-impl"
version = "0.3.0"
source = "git+https://git.libre-chip.org/libre-chip/fayalite.git?branch=master#cf3e6cfc6bc33eebf2d2862c7a1948b9cf40ecac"
source = "git+https://git.libre-chip.org/libre-chip/fayalite.git?branch=master#31353862ceba3d255fd6712813a457688b269358"
dependencies = [
"base16ct 0.2.0",
"num-bigint",
@ -440,7 +440,7 @@ dependencies = [
[[package]]
name = "fayalite-visit-gen"
version = "0.3.0"
source = "git+https://git.libre-chip.org/libre-chip/fayalite.git?branch=master#cf3e6cfc6bc33eebf2d2862c7a1948b9cf40ecac"
source = "git+https://git.libre-chip.org/libre-chip/fayalite.git?branch=master#31353862ceba3d255fd6712813a457688b269358"
dependencies = [
"indexmap",
"prettyplease",

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

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