writing VCD for combinatorial circuits works!

crates/fayalite/src/sim.rs

@@ -3620,6 +3620,7 @@ struct SimulationImpl {
     uninitialized_inputs: HashSet<Target>,
     io_targets: HashMap<Target, CompiledValue<CanonicalType>>,
     made_initial_step: bool,
+    needs_settle: bool,
     trace_decls: TraceModule,
     traces: Box<[SimTrace<BitVec>]>,
     trace_writers: Vec<TraceWriterState<DynTraceWriterDecls>>,
@@ -3669,6 +3670,7 @@ impl SimulationImpl {
             uninitialized_inputs: HashSet::new(),
             io_targets: HashMap::new(),
             made_initial_step: false,
+            needs_settle: true,
             trace_decls: compiled.base_module.trace_decls,
             traces: Box::from_iter(compiled.traces.iter().map(
                 |&SimTrace {
@@ -3804,9 +3806,7 @@ impl SimulationImpl {
     }
     #[track_caller]
     fn advance_time(&mut self, duration: SimDuration) {
-        if !self.made_initial_step {
-            self.settle_step();
-        }
+        self.settle_step();
         self.instant += duration;
         self.for_each_trace_writer_storing_error(|this, mut trace_writer_state| {
             match &mut trace_writer_state {
@@ -3825,6 +3825,9 @@ impl SimulationImpl {
             self.uninitialized_inputs.is_empty(),
             "didn't initialize all inputs",
         );
+        if !self.needs_settle {
+            return;
+        }
         self.state.setup_call(0);
         self.state.run();
         if self.made_initial_step {
@@ -3833,6 +3836,7 @@ impl SimulationImpl {
             self.read_traces::<true>();
         }
         self.made_initial_step = true;
+        self.needs_settle = false;
         self.for_each_trace_writer_storing_error(|this, trace_writer_state| {
             Ok(match trace_writer_state {
                 TraceWriterState::Decls(trace_writer_decls) => TraceWriterState::Running(
@@ -3861,12 +3865,14 @@ impl SimulationImpl {
         panic!("simulator read/write expression must not have dynamic array indexes");
     }
     #[track_caller]
-    fn read_bool_or_int<I: BoolOrIntType>(&self, io: Expr<I>) -> I::Value {
+    fn read_bool_or_int<I: BoolOrIntType>(&mut self, io: Expr<I>) -> I::Value {
         let Some(target) = io.target() else {
             panic!("can't read from expression that's not a field/element of `Simulation::io()`");
         };
         let compiled_value = self.get_io(*target);
-        if !self.made_initial_step {
+        if self.made_initial_step {
+            self.settle_step();
+        } else {
             match target.flow() {
                 Flow::Source => {
                     panic!("can't read from an output before the simulation has made any steps");
@@ -3906,6 +3912,7 @@ impl SimulationImpl {
         if !self.made_initial_step {
             self.uninitialized_inputs.remove(&*target);
         }
+        self.needs_settle = true;
         match compiled_value.range.len() {
             TypeLen::A_SMALL_SLOT => {
                 self.state.small_slots[compiled_value.range.small_slots.start] =
@@ -3981,9 +3988,15 @@ impl SimulationImpl {
         retval
     }
     fn close(mut self) -> std::io::Result<()> {
+        if self.made_initial_step {
+            self.settle_step();
+        }
         self.close_all_trace_writers()
     }
     fn flush_traces(&mut self) -> std::io::Result<()> {
+        if self.made_initial_step {
+            self.settle_step();
+        }
         self.for_each_trace_writer_getting_error(
             |this, trace_writer: TraceWriterState<DynTraceWriterDecls>| match trace_writer {
                 TraceWriterState::Decls(v) => {
@@ -4068,6 +4081,7 @@ impl<T: BundleType> fmt::Debug for Simulation<T> {
                     uninitialized_inputs,
                     io_targets,
                     made_initial_step,
+                    needs_settle,
                     trace_decls,
                     traces,
                     trace_writers,
@@ -4084,6 +4098,7 @@ impl<T: BundleType> fmt::Debug for Simulation<T> {
             )
             .field("io_targets", &SortedMapDebug(io_targets))
             .field("made_initial_step", made_initial_step)
+            .field("needs_settle", needs_settle)
             .field("trace_decls", trace_decls)
             .field("traces", traces)
             .field("trace_writers", trace_writers)
@@ -4140,7 +4155,7 @@ impl<T: BundleType> Simulation<T> {
         self.sim_impl.advance_time(duration);
     }
     #[track_caller]
-    pub fn read_bool_or_int<I: BoolOrIntType>(&self, io: Expr<I>) -> I::Value {
+    pub fn read_bool_or_int<I: BoolOrIntType>(&mut self, io: Expr<I>) -> I::Value {
         self.sim_impl.read_bool_or_int(io)
     }
     #[track_caller]

crates/fayalite/tests/formal.rs

@@ -0,0 +1,133 @@
+// SPDX-License-Identifier: LGPL-3.0-or-later
+// See Notices.txt for copyright information
+//! Formal tests in Fayalite
+
+use fayalite::{
+    cli::FormalMode,
+    clock::{Clock, ClockDomain},
+    expr::{CastTo, HdlPartialEq},
+    firrtl::ExportOptions,
+    formal::{any_seq, formal_reset, hdl_assert, hdl_assume},
+    hdl_module,
+    int::{Bool, UInt},
+    module::{connect, connect_any, reg_builder, wire},
+    reset::ToReset,
+    testing::assert_formal,
+};
+
+/// Test hidden state
+///
+/// Hidden state can cause problems for induction, since the formal engine
+/// can assign invalid values to the state registers, making it traverse
+/// valid but unreachable states.
+///
+/// One solution is to go sufficiently in the past so the engine is forced
+/// to eventually take a reachable state. This may be hampered by
+/// existence of loops, then assumptions may be added to break them.
+///
+/// Another solution is to "open the black box" and add additional
+/// assertions involving the hidden state, so that the unreachable states
+/// become invalid as well.
+///
+/// Both approaches are taken here.
+///
+/// See [Claire Wolf's presentation] and [Zipcpu blog article].
+///
+/// [Claire Wolf's presentation]: https://web.archive.org/web/20200115081517fw_/http://www.clifford.at/papers/2017/smtbmc-sby/
+/// [Zipcpu blog article]: https://zipcpu.com/blog/2018/03/10/induction-exercise.html
+mod hidden_state {
+    use super::*;
+    /// Test hidden state by shift registers
+    ///
+    /// The code implement the ideas from an article in the [Zipcpu blog]. Two
+    /// shift registers are fed from the same input, so they should always have
+    /// the same value. However the only observable is a comparison of their
+    /// last bit, all the others are hidden. To complicate matters, an enable
+    /// signal causes a loop in state space.
+    ///
+    /// [Zipcpu blog]: https://zipcpu.com/blog/2018/03/10/induction-exercise.html
+    #[test]
+    fn shift_register() {
+        enum ConstraintMode {
+            WithExtraAssertions,
+            WithExtraAssumptions,
+        }
+        use ConstraintMode::*;
+        #[hdl_module]
+        fn test_module(constraint_mode: ConstraintMode) {
+            #[hdl]
+            let clk: Clock = m.input();
+            #[hdl]
+            let cd = wire();
+            connect(
+                cd,
+                #[hdl]
+                ClockDomain {
+                    clk,
+                    rst: formal_reset().to_reset(),
+                },
+            );
+            // input signal for the shift registers
+            #[hdl]
+            let i: Bool = wire();
+            connect(i, any_seq(Bool));
+            // shift enable signal
+            #[hdl]
+            let en: Bool = wire();
+            connect(en, any_seq(Bool));
+            // comparison output
+            #[hdl]
+            let o: Bool = wire();
+            // shift registers, with enable
+            #[hdl]
+            let r1 = reg_builder().clock_domain(cd).reset(0u8);
+            #[hdl]
+            let r2 = reg_builder().clock_domain(cd).reset(0u8);
+            #[hdl]
+            if en {
+                connect_any(r1, (r1 << 1) | i.cast_to(UInt[1]));
+                connect_any(r2, (r2 << 1) | i.cast_to(UInt[1]));
+            }
+            // compare last bits of both shift registers
+            connect(o, r1[7].cmp_eq(r2[7]));
+
+            // what we want to prove: last bits are always equal
+            hdl_assert(clk, o, "");
+
+            // additional terms below are only needed to assist with the induction proof
+            match constraint_mode {
+                WithExtraAssertions => {
+                    // "Open the box": add assertions about hidden state.
+                    // In this case, the hidden bits are also always equal.
+                    hdl_assert(clk, r1.cmp_eq(r2), "");
+                }
+                WithExtraAssumptions => {
+                    // Break the loop, do not allow "en" to remain low forever
+                    #[hdl]
+                    let past_en_reg = reg_builder().clock_domain(cd).reset(false);
+                    connect(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,
+        // given that we are allowed to disable the shift once every two cycles.
+        assert_formal(
+            "shift_register_with_assumptions",
+            test_module(WithExtraAssumptions),
+            FormalMode::Prove,
+            16,
+            None,
+            ExportOptions::default(),
+        );
+        // here a couple of cycles is enough
+        assert_formal(
+            "shift_register_with_assertions",
+            test_module(WithExtraAssertions),
+            FormalMode::Prove,
+            2,
+            None,
+            ExportOptions::default(),
+        );
+    }
+}

crates/fayalite/tests/sim.rs

@@ -120,6 +120,7 @@ fn test_connect_const() {
         },
     },
     made_initial_step: true,
+    needs_settle: false,
     trace_decls: TraceModule {
         name: "connect_const",
         children: [
@@ -182,7 +183,6 @@ pub fn mod1() {
     connect(o, child);
 }
 
-#[cfg(todo)]
 #[hdl]
 #[test]
 fn test_mod1() {
@@ -195,10 +195,58 @@ fn test_mod1() {
     sim.advance_time(SimDuration::from_micros(1));
     sim.write_bool_or_int(sim.io().o.i, 0xA_hdl_u4);
     sim.advance_time(SimDuration::from_micros(1));
+    sim.flush_traces().unwrap();
     let vcd = String::from_utf8(writer.take()).unwrap();
     println!("####### VCD:\n{vcd}\n#######");
-    todo!("generated vcd is incorrect");
-    if vcd != r#""# {
+    if vcd
+        != r#"$timescale 1 ps $end
+$scope module mod1 $end
+$scope struct o $end
+$var wire 4 ! i $end
+$var wire 2 " o $end
+$var wire 2 # i2 $end
+$var wire 4 $ o2 $end
+$upscope $end
+$scope struct child $end
+$var wire 4 ) i $end
+$var wire 2 * o $end
+$var wire 2 + i2 $end
+$var wire 4 , o2 $end
+$upscope $end
+$scope module mod1_child $end
+$var wire 4 % i $end
+$var wire 2 & o $end
+$var wire 2 ' i2 $end
+$var wire 4 ( o2 $end
+$upscope $end
+$upscope $end
+$enddefinitions $end
+$dumpvars
+b11 !
+b11 "
+b10 #
+b1110 $
+b11 %
+b11 &
+b10 '
+b1110 (
+b11 )
+b11 *
+b10 +
+b1110 ,
+$end
+#1000000
+b1010 !
+b10 "
+b1111 $
+b1010 %
+b10 &
+b1111 (
+b1010 )
+b10 *
+b1111 ,
+#2000000
+"# {
         panic!();
     }
     let sim_debug = format!("{sim:#?}");
@@ -718,6 +766,7 @@ fn test_mod1() {
         },
     },
     made_initial_step: true,
+    needs_settle: false,
     trace_decls: TraceModule {
         name: "mod1",
         children: [
@@ -887,7 +936,7 @@ fn test_mod1() {
                 ty: UInt<4>,
             },
             state: 0xa,
-            last_state: 0xa,
+            last_state: 0x3,
         },
         SimTrace {
             id: TraceScalarId(1),
@@ -896,7 +945,7 @@ fn test_mod1() {
                 ty: SInt<2>,
             },
             state: 0x2,
-            last_state: 0x2,
+            last_state: 0x3,
         },
         SimTrace {
             id: TraceScalarId(2),
@@ -914,7 +963,7 @@ fn test_mod1() {
                 ty: UInt<4>,
             },
             state: 0xf,
-            last_state: 0xf,
+            last_state: 0xe,
         },
         SimTrace {
             id: TraceScalarId(4),
@@ -923,7 +972,7 @@ fn test_mod1() {
                 ty: UInt<4>,
             },
             state: 0xa,
-            last_state: 0xa,
+            last_state: 0x3,
         },
         SimTrace {
             id: TraceScalarId(5),
@@ -932,7 +981,7 @@ fn test_mod1() {
                 ty: SInt<2>,
             },
             state: 0x2,
-            last_state: 0x2,
+            last_state: 0x3,
         },
         SimTrace {
             id: TraceScalarId(6),
@@ -950,7 +999,7 @@ fn test_mod1() {
                 ty: UInt<4>,
             },
             state: 0xf,
-            last_state: 0xf,
+            last_state: 0xe,
         },
         SimTrace {
             id: TraceScalarId(8),
@@ -959,7 +1008,7 @@ fn test_mod1() {
                 ty: UInt<4>,
             },
             state: 0xa,
-            last_state: 0xa,
+            last_state: 0x3,
         },
         SimTrace {
             id: TraceScalarId(9),
@@ -968,7 +1017,7 @@ fn test_mod1() {
                 ty: SInt<2>,
             },
             state: 0x2,
-            last_state: 0x2,
+            last_state: 0x3,
         },
         SimTrace {
             id: TraceScalarId(10),
@@ -986,11 +1035,19 @@ fn test_mod1() {
                 ty: UInt<4>,
             },
             state: 0xf,
-            last_state: 0xf,
+            last_state: 0xe,
         },
     ],
-    trace_writers: [],
-    instant: 0 s,
+    trace_writers: [
+        Running(
+            VcdWriter {
+                finished_init: true,
+                timescale: 1 ps,
+                ..
+            },
+        ),
+    ],
+    instant: 2 μs,
 }"# {
         panic!();
     }