From 0d54b9a2a9abd7c8b34566ae6e55ca0d508c6a21 Mon Sep 17 00:00:00 2001 From: Jacob Lifshay Date: Thu, 3 Oct 2024 23:07:14 -0700 Subject: [PATCH] queue formal proof passes! --- crates/fayalite/src/cli.rs | 2 +- crates/fayalite/src/formal.rs | 70 +++++++++- crates/fayalite/src/prelude.rs | 5 +- crates/fayalite/src/testing.rs | 4 +- crates/fayalite/src/util/ready_valid.rs | 170 +++++++++++++++--------- crates/fayalite/tests/module.rs | 18 +-- 6 files changed, 183 insertions(+), 86 deletions(-) diff --git a/crates/fayalite/src/cli.rs b/crates/fayalite/src/cli.rs index b0b818c..f1d69d2 100644 --- a/crates/fayalite/src/cli.rs +++ b/crates/fayalite/src/cli.rs @@ -516,7 +516,7 @@ impl FormalArgs { std::fs::write(&sby_file, self.sby_contents(&output)?)?; let mut cmd = process::Command::new(&self.sby); cmd.arg("-f"); - cmd.arg(sby_file); + cmd.arg(sby_file.file_name().unwrap()); cmd.args(&self.sby_extra_args); cmd.current_dir(&output.verilog.firrtl.output_dir); let status = self.verilog.firrtl.base.run_external_command(cmd)?; diff --git a/crates/fayalite/src/formal.rs b/crates/fayalite/src/formal.rs index eab1969..17d3122 100644 --- a/crates/fayalite/src/formal.rs +++ b/crates/fayalite/src/formal.rs @@ -1,7 +1,8 @@ // SPDX-License-Identifier: LGPL-3.0-or-later // See Notices.txt for copyright information use crate::{ - intern::{Intern, Interned}, + int::BoolOrIntType, + intern::{Intern, Interned, Memoize}, prelude::*, }; use std::sync::OnceLock; @@ -172,12 +173,7 @@ pub fn formal_reset() -> Expr { m.annotate_module(BlackBoxInlineAnnotation { path: "fayalite_formal_reset.v".intern(), text: r"module __fayalite_formal_reset(output rst); - reg rst; - (* gclk *) - reg gclk; - initial rst = 1; - always @(posedge gclk) - rst <= 0; + assign rst = $initstate; endmodule " .intern(), @@ -189,3 +185,63 @@ endmodule let formal_reset = instance(*MOD.get_or_init(formal_reset)); formal_reset.rst } + +macro_rules! make_any_const_fn { + ($ident:ident, $verilog_attribute:literal) => { + #[hdl] + pub fn $ident(ty: T) -> Expr { + #[hdl_module(extern)] + pub(super) fn $ident(ty: T) { + #[hdl] + let out: T = m.output(ty); + let width = ty.width(); + let verilog_bitslice = if width == 1 { + String::new() + } else { + format!(" [{}:0]", width - 1) + }; + m.annotate_module(BlackBoxInlineAnnotation { + path: Intern::intern_owned(format!( + "fayalite_{}_{width}.v", + stringify!($ident), + )), + text: Intern::intern_owned(format!( + r"module __fayalite_{}_{width}(output{verilog_bitslice} out); + (* {} *) + reg{verilog_bitslice} out; +endmodule +", + stringify!($ident), + $verilog_attribute, + )), + }); + m.verilog_name(format!("__fayalite_{}_{width}", stringify!($ident))); + } + #[derive(Copy, Clone, PartialEq, Eq, Hash)] + struct TheMemoize(T); + impl Memoize for TheMemoize { + type Input = (); + type InputOwned = (); + type Output = Option>>>; + fn inner(self, _input: &Self::Input) -> Self::Output { + if self.0.width() == 0 { + None + } else { + Some($ident(self.0)) + } + } + } + let Some(module) = TheMemoize(ty).get_owned(()) else { + return 0_hdl_u0.cast_bits_to(ty); + }; + #[hdl] + let $ident = instance(module); + $ident.out + } + }; +} + +make_any_const_fn!(any_const, "anyconst"); +make_any_const_fn!(any_seq, "anyseq"); +make_any_const_fn!(all_const, "allconst"); +make_any_const_fn!(all_seq, "allseq"); diff --git a/crates/fayalite/src/prelude.rs b/crates/fayalite/src/prelude.rs index f1a9736..46d9e6e 100644 --- a/crates/fayalite/src/prelude.rs +++ b/crates/fayalite/src/prelude.rs @@ -14,8 +14,9 @@ pub use crate::{ ReduceBits, ToExpr, }, formal::{ - formal_global_clock, formal_reset, hdl_assert, hdl_assert_with_enable, hdl_assume, - hdl_assume_with_enable, hdl_cover, hdl_cover_with_enable, MakeFormalExpr, + all_const, all_seq, any_const, any_seq, formal_global_clock, formal_reset, hdl_assert, + hdl_assert_with_enable, hdl_assume, hdl_assume_with_enable, hdl_cover, + hdl_cover_with_enable, MakeFormalExpr, }, hdl, hdl_module, int::{Bool, DynSize, KnownSize, SInt, SIntType, Size, UInt, UIntType}, diff --git a/crates/fayalite/src/testing.rs b/crates/fayalite/src/testing.rs index 07252f1..4517e34 100644 --- a/crates/fayalite/src/testing.rs +++ b/crates/fayalite/src/testing.rs @@ -68,7 +68,6 @@ fn get_assert_formal_target_path(test_name: &dyn std::fmt::Display) -> PathBuf { }, ); let mut dir = String::with_capacity(64); - write!(dir, "{simple_hash:08x}-").unwrap(); for ch in Path::new(file) .file_stem() .unwrap_or_default() @@ -84,6 +83,7 @@ fn get_assert_formal_target_path(test_name: &dyn std::fmt::Display) -> PathBuf { _ => '_', }); } + write!(dir, "-{simple_hash:08x}").unwrap(); let index = *DIRS .lock() .unwrap() @@ -91,7 +91,7 @@ fn get_assert_formal_target_path(test_name: &dyn std::fmt::Display) -> PathBuf { .entry_ref(&dir) .and_modify(|v| *v += 1) .or_insert(0); - write!(dir, ".{index}").unwrap(); + write!(dir, "-{index}").unwrap(); get_cargo_target_dir() .join("fayalite_assert_formal") .join(dir) diff --git a/crates/fayalite/src/util/ready_valid.rs b/crates/fayalite/src/util/ready_valid.rs index 41299a6..f3d5653 100644 --- a/crates/fayalite/src/util/ready_valid.rs +++ b/crates/fayalite/src/util/ready_valid.rs @@ -49,7 +49,6 @@ impl ReadyValid { } } -// TODO: needs testing #[hdl_module] pub fn queue( ty: T, @@ -134,7 +133,7 @@ pub fn queue( #[hdl] if inp_fire { #[hdl] - if inp_index.cmp_eq(capacity) { + if inp_index.cmp_eq(capacity.get() - 1) { connect_any(inp_index, 0_hdl_u0); } else { connect_any(inp_index, inp_index + 1_hdl_u1); @@ -144,7 +143,7 @@ pub fn queue( #[hdl] if out_fire { #[hdl] - if out_index.cmp_eq(capacity) { + if out_index.cmp_eq(capacity.get() - 1) { connect_any(out_index, 0_hdl_u0); } else { connect_any(out_index, out_index + 1_hdl_u1); @@ -153,10 +152,12 @@ pub fn queue( #[hdl] if indexes_equal { - connect( - count, - maybe_full.cast_to_static::>() << (count_ty.width() - 1), - ); + #[hdl] + if maybe_full { + connect_any(count, capacity); + } else { + connect_any(count, 0_hdl_u0); + } } else { if capacity.is_power_of_two() { debug_assert_eq!(count_ty.width(), index_ty.width() + 1); @@ -182,6 +183,7 @@ mod tests { use crate::{ cli::FormalMode, firrtl::ExportOptions, module::transform::simplify_enums::SimplifyEnumsKind, testing::assert_formal, + ty::StaticType, }; use std::num::NonZero; @@ -190,8 +192,8 @@ mod tests { assert_formal( format_args!("test_queue_{capacity}_{inp_ready_is_comb}_{out_valid_is_comb}"), queue_test(capacity, inp_ready_is_comb, out_valid_is_comb), - FormalMode::BMC, - 20, + FormalMode::Prove, + 14, None, ExportOptions { simplify_enums: Some(SimplifyEnumsKind::ReplaceWithBundleOfUInts), @@ -200,12 +202,6 @@ mod tests { ); #[hdl_module] fn queue_test(capacity: NonZeroUsize, inp_ready_is_comb: bool, out_valid_is_comb: bool) { - #[hdl] - let inp_data: HdlOption> = m.input(); - #[hdl] - let out_ready: Bool = m.input(); - #[hdl] - let start_check: Bool = m.input(); #[hdl] let clk: Clock = m.input(); #[hdl] @@ -219,6 +215,24 @@ mod tests { }, ); #[hdl] + let inp_data: HdlOption> = wire(); + #[hdl] + if any_seq(Bool) { + connect(inp_data, HdlSome(any_seq(UInt::<8>::TYPE))); + } else { + connect(inp_data, HdlNone()); + } + #[hdl] + let out_ready: Bool = wire(); + connect(out_ready, any_seq(Bool)); + let index_ty: UInt<32> = UInt::TYPE; + #[hdl] + let index_to_check = wire(); + connect(index_to_check, any_const(index_ty)); + let index_max = !index_ty.zero(); + // we saturate at index_max, so only check indexes where we properly maintain position + hdl_assume(clk, index_to_check.cmp_ne(index_max), ""); + #[hdl] let dut = instance(queue( UInt[ConstUsize::<8>], capacity, @@ -228,63 +242,97 @@ mod tests { connect(dut.cd, cd); connect(dut.inp.data, inp_data); connect(dut.out.ready, out_ready); + hdl_assume( + clk, + index_to_check.cmp_ne(!Expr::ty(index_to_check).zero()), + "", + ); + #[hdl] - let count = reg_builder().clock_domain(cd).reset(0u32); + let expected_count = reg_builder().clock_domain(cd).reset(0u32); #[hdl] - let next_count = wire(); - connect(next_count, count); - connect(count, next_count); + let next_expected_count = wire(); + connect(next_expected_count, expected_count); + connect(expected_count, next_expected_count); #[hdl] if ReadyValid::fire(dut.inp) & !ReadyValid::fire(dut.out) { - connect_any(next_count, count + 1u8); + connect_any(next_expected_count, expected_count + 1u8); } else if !ReadyValid::fire(dut.inp) & ReadyValid::fire(dut.out) { - connect_any(next_count, count - 1u8); + connect_any(next_expected_count, expected_count - 1u8); } - hdl_assert(cd.clk, count.cmp_eq(dut.count), ""); + hdl_assert(cd.clk, expected_count.cmp_eq(dut.count), ""); + #[hdl] - let started_check = reg_builder().clock_domain(cd).reset(false); + let prev_out_ready = reg_builder().clock_domain(cd).reset(!0_hdl_u3); + connect_any( + prev_out_ready, + (prev_out_ready << 1) | out_ready.cast_to(UInt[1]), + ); #[hdl] - let steps_till_output = reg_builder().clock_domain(cd).reset(0u32); + let prev_inp_valid = reg_builder().clock_domain(cd).reset(!0_hdl_u3); + connect_any( + prev_inp_valid, + (prev_inp_valid << 1) | HdlOption::is_some(inp_data).cast_to(UInt[1]), + ); + hdl_assume(clk, (prev_out_ready & prev_inp_valid).cmp_ne(0u8), ""); + #[hdl] - let expected_output = reg_builder().clock_domain(cd).reset(HdlNone()); + let inp_index = reg_builder().clock_domain(cd).reset(index_ty.zero()); #[hdl] - if start_check & !started_check { + let stored_inp_data = reg_builder().clock_domain(cd).reset(0u8); + + #[hdl] + if let HdlSome(data) = ReadyValid::fire_data(dut.inp) { #[hdl] - if let HdlSome(inp) = ReadyValid::fire_data(dut.inp) { - connect(started_check, true); - connect_any( - steps_till_output, - count + (!ReadyValid::fire(dut.out)).cast_to(UInt[1]), - ); - connect(expected_output, HdlSome(inp)); - } - } else if started_check & steps_till_output.cmp_ne(0u32) & ReadyValid::fire(dut.out) { - connect_any(steps_till_output, steps_till_output - 1u32); - } - #[hdl] - let stored_output = reg_builder().clock_domain(cd).reset(HdlNone()); - #[hdl] - if let HdlSome(out) = ReadyValid::fire_data(dut.out) { - #[hdl] - if (start_check & !started_check) | (started_check & steps_till_output.cmp_ne(0u32)) - { - connect(stored_output, HdlSome(out)); - } - } - #[hdl] - if started_check & steps_till_output.cmp_eq(0u32) { - #[hdl] - if let HdlSome(expected_output) = expected_output { + if inp_index.cmp_lt(index_max) { + connect_any(inp_index, inp_index + 1u8); #[hdl] - if let HdlSome(stored_output) = stored_output { - hdl_assert(cd.clk, stored_output.cmp_eq(expected_output), ""); - } else { - hdl_assert(cd.clk, false.to_expr(), ""); + if inp_index.cmp_eq(index_to_check) { + connect(stored_inp_data, data); } - } else { - hdl_assert(cd.clk, false.to_expr(), ""); } } + + #[hdl] + if inp_index.cmp_lt(index_to_check) { + hdl_assert(clk, stored_inp_data.cmp_eq(0u8), ""); + } + + #[hdl] + let out_index = reg_builder().clock_domain(cd).reset(index_ty.zero()); + #[hdl] + let stored_out_data = reg_builder().clock_domain(cd).reset(0u8); + + #[hdl] + if let HdlSome(data) = ReadyValid::fire_data(dut.out) { + #[hdl] + if out_index.cmp_lt(index_max) { + connect_any(out_index, out_index + 1u8); + #[hdl] + if out_index.cmp_eq(index_to_check) { + connect(stored_out_data, data); + } + } + } + + #[hdl] + if out_index.cmp_lt(index_to_check) { + hdl_assert(clk, stored_out_data.cmp_eq(0u8), ""); + } + + hdl_assert(clk, inp_index.cmp_ge(out_index), ""); + + #[hdl] + if inp_index.cmp_lt(index_max) & out_index.cmp_lt(index_max) { + hdl_assert(clk, expected_count.cmp_eq(inp_index - out_index), ""); + } else { + hdl_assert(clk, expected_count.cmp_ge(inp_index - out_index), ""); + } + + #[hdl] + if inp_index.cmp_gt(index_to_check) & out_index.cmp_gt(index_to_check) { + hdl_assert(clk, stored_inp_data.cmp_eq(stored_out_data), ""); + } } } @@ -328,49 +376,41 @@ mod tests { test_queue(NonZero::new(2).unwrap(), true, true); } - #[cfg(todo)] #[test] fn test_3_false_false() { test_queue(NonZero::new(3).unwrap(), false, false); } - #[cfg(todo)] #[test] fn test_3_false_true() { test_queue(NonZero::new(3).unwrap(), false, true); } - #[cfg(todo)] #[test] fn test_3_true_false() { test_queue(NonZero::new(3).unwrap(), true, false); } - #[cfg(todo)] #[test] fn test_3_true_true() { test_queue(NonZero::new(3).unwrap(), true, true); } - #[cfg(todo)] #[test] fn test_4_false_false() { test_queue(NonZero::new(4).unwrap(), false, false); } - #[cfg(todo)] #[test] fn test_4_false_true() { test_queue(NonZero::new(4).unwrap(), false, true); } - #[cfg(todo)] #[test] fn test_4_true_false() { test_queue(NonZero::new(4).unwrap(), true, false); } - #[cfg(todo)] #[test] fn test_4_true_true() { test_queue(NonZero::new(4).unwrap(), true, true); diff --git a/crates/fayalite/tests/module.rs b/crates/fayalite/tests/module.rs index 7d12739..0d690f2 100644 --- a/crates/fayalite/tests/module.rs +++ b/crates/fayalite/tests/module.rs @@ -3394,7 +3394,7 @@ circuit check_formal: %[[ { "class": "firrtl.transforms.BlackBoxInlineAnno", "name": "fayalite_formal_reset.v", - "text": "module __fayalite_formal_reset(output rst);\n reg rst;\n (* gclk *)\n reg gclk;\n initial rst = 1;\n always @(posedge gclk)\n rst <= 0;\nendmodule\n", + "text": "module __fayalite_formal_reset(output rst);\n assign rst = $initstate;\nendmodule\n", "target": "~check_formal|formal_reset" } ]] @@ -3407,20 +3407,20 @@ circuit check_formal: %[[ input pred1: UInt<1> @[module-XXXXXXXXXX.rs 6:1] input pred2: UInt<1> @[module-XXXXXXXXXX.rs 7:1] input pred3: UInt<1> @[module-XXXXXXXXXX.rs 8:1] - inst formal_reset of formal_reset @[formal.rs 189:24] + inst formal_reset of formal_reset @[formal.rs 185:24] assert(clk, pred1, and(en1, not(formal_reset.rst)), "en check 1") @[module-XXXXXXXXXX.rs 9:1] - inst formal_reset_1 of formal_reset @[formal.rs 189:24] + inst formal_reset_1 of formal_reset @[formal.rs 185:24] assume(clk, pred2, and(en2, not(formal_reset_1.rst)), "en check 2") @[module-XXXXXXXXXX.rs 10:1] - inst formal_reset_2 of formal_reset @[formal.rs 189:24] + inst formal_reset_2 of formal_reset @[formal.rs 185:24] cover(clk, pred3, and(en3, not(formal_reset_2.rst)), "en check 3") @[module-XXXXXXXXXX.rs 11:1] - inst formal_reset_3 of formal_reset @[formal.rs 189:24] + inst formal_reset_3 of formal_reset @[formal.rs 185:24] assert(clk, pred1, and(UInt<1>(0h1), not(formal_reset_3.rst)), "check 1") @[module-XXXXXXXXXX.rs 12:1] - inst formal_reset_4 of formal_reset @[formal.rs 189:24] + inst formal_reset_4 of formal_reset @[formal.rs 185:24] assume(clk, pred2, and(UInt<1>(0h1), not(formal_reset_4.rst)), "check 2") @[module-XXXXXXXXXX.rs 13:1] - inst formal_reset_5 of formal_reset @[formal.rs 189:24] + inst formal_reset_5 of formal_reset @[formal.rs 185:24] cover(clk, pred3, and(UInt<1>(0h1), not(formal_reset_5.rst)), "check 3") @[module-XXXXXXXXXX.rs 14:1] - extmodule formal_reset: @[formal.rs 168:5] - output rst: UInt<1> @[formal.rs 171:32] + extmodule formal_reset: @[formal.rs 169:5] + output rst: UInt<1> @[formal.rs 172:32] defname = __fayalite_formal_reset "#, };