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

Compare commits

base: libre-chip:c1f1a8b74982965acb86274d1a621fcdb1a4d751
Branches Tags
libre-chip:master
libre-chip:square-brackets-generics-experiment
libre-chip:runtime-generics
libre-chip:type-deduction
libre-chip:v0.2.0
libre-chip:v0.1.0
..
compare: libre-chip:39d895764ab07188885d9f4728db161101d6a6e4
Branches Tags
libre-chip:master
libre-chip:square-brackets-generics-experiment
libre-chip:runtime-generics
libre-chip:type-deduction
libre-chip:v0.2.0
libre-chip:v0.1.0

1 commit
c1f1a8b749 ... 39d895764a

Author SHA1 Message Date
Cesar Strauss
39d895764a Add test module exercising formal verification.
All checks were successful
/ deps (pull_request) Successful in 16s
Details
/ test (pull_request) Successful in 4m49s
Details
2024-11-20 17:39:00 -03:00
1 changed files with 11 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

6
crates/fayalite/tests/formal.rs
View file

@ -95,13 +95,12 @@ mod hidden_state {
hdl_assert(clk, o, ""); hdl_assert(clk, o, "");
// additional terms below are only needed to assist with the induction proof // additional terms below are only needed to assist with the induction proof
match constraint_mode { if let WithExtraAssertions = constraint_mode {
WithExtraAssertions => {
// "Open the box": add assertions about hidden state. // "Open the box": add assertions about hidden state.
// In this case, the hidden bits are also always equal. // In this case, the hidden bits are also always equal.
hdl_assert(clk, r1.cmp_eq(r2), ""); hdl_assert(clk, r1.cmp_eq(r2), "");
} }
WithExtraAssumptions => { if let WithExtraAssumptions = constraint_mode {
// Break the loop, do not allow "en" to remain low forever // Break the loop, do not allow "en" to remain low forever
#[hdl] #[hdl]
let past_en_reg = reg_builder().clock_domain(cd).reset(false); let past_en_reg = reg_builder().clock_domain(cd).reset(false);
@ -109,7 +108,6 @@ mod hidden_state {
hdl_assume(clk, past_en_reg | en, ""); hdl_assume(clk, past_en_reg | en, "");
} }
} }
}
// we need a minimum of 16 steps so we can constrain all eight shift register bits, // we need a minimum of 16 steps so we can constrain all eight shift register bits,
// given that we are allowed to disable the shift once every two cycles. // given that we are allowed to disable the shift once every two cycles.
assert_formal( assert_formal(