From 9fe2b52662df0b2a1c7d8a975b05b18173f30b2d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Kevin=20L=C3=A4ufer?= Date: Mon, 18 Dec 2023 12:31:12 -0500 Subject: [PATCH] tb: add option to encode i/o constraints as single assert --- synth/src/testbench.rs | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) diff --git a/synth/src/testbench.rs b/synth/src/testbench.rs index e77e2f9..86f306f 100644 --- a/synth/src/testbench.rs +++ b/synth/src/testbench.rs @@ -298,8 +298,12 @@ impl Testbench { let range = self.step_range(step_id); let words = &self.data[range]; + // we can encode everything into a single assert or into multiple asserts + let single_assert = false; + // apply all io constraints in this step let mut offset = 0; + let mut constraints = Vec::with_capacity(self.ios.len()); for io in self.ios.iter() { let io_words = &words[offset..(offset + io.words)]; if !is_x(io_words) { @@ -308,10 +312,18 @@ impl Testbench { let value = ValueRef::new(non_x_words, io.width).to_bit_string(); let value_expr = bit_string_to_smt(smt_ctx, &value); let io_at_step = enc.get_at(ctx, smt_ctx, io.expr, step_id); - smt_ctx.assert(smt_ctx.eq(io_at_step, value_expr))?; + let constraint = smt_ctx.eq(io_at_step, value_expr); + if single_assert { + constraints.push(constraint); + } else { + smt_ctx.assert(constraint)?; + } } offset += io.words; } + if !constraints.is_empty() { + smt_ctx.assert(smt_ctx.and_many(constraints))?; + } } Ok(()) }