Skip to content

Commit 7eaa4bc

Browse files
committed
sim: Add -noinitstate option and handle non-cosim initstate
This adds the -noinitstate option which is required to simulate counterexamples to induction with yw-cosim. Also add handling for $initstate cells for non-co-simulation.
1 parent 2002490 commit 7eaa4bc

File tree

1 file changed

+14
-1
lines changed

1 file changed

+14
-1
lines changed

passes/sat/sim.cc

+14-1
Original file line numberDiff line numberDiff line change
@@ -111,6 +111,7 @@ struct SimShared
111111
int step = 0;
112112
std::vector<TriggeredAssertion> triggered_assertions;
113113
bool serious_asserts = false;
114+
bool initstate = true;
114115
};
115116

116117
void zinit(State &v)
@@ -1356,6 +1357,8 @@ struct SimWorker : SimShared
13561357
set_inports(clock, State::Sx);
13571358
set_inports(clockn, State::Sx);
13581359

1360+
top->set_initstate_outputs(initstate ? State::S1 : State::S0);
1361+
13591362
update(false);
13601363

13611364
register_output_step(0);
@@ -1372,6 +1375,9 @@ struct SimWorker : SimShared
13721375
update(true);
13731376
register_output_step(10*cycle + 5);
13741377

1378+
if (cycle == 0)
1379+
top->set_initstate_outputs(State::S0);
1380+
13751381
if (debug)
13761382
log("\n===== %d =====\n", 10*cycle + 10);
13771383
else if (verbose)
@@ -1953,7 +1959,7 @@ struct SimWorker : SimShared
19531959
if (yw.steps.empty()) {
19541960
log_warning("Yosys witness file `%s` contains no time steps\n", yw.filename.c_str());
19551961
} else {
1956-
top->set_initstate_outputs(State::S1);
1962+
top->set_initstate_outputs(initstate ? State::S1 : State::S0);
19571963
set_yw_state(yw, hierarchy, 0);
19581964
set_yw_clocks(yw, hierarchy, true);
19591965
initialize_stable_past();
@@ -2546,6 +2552,9 @@ struct SimPass : public Pass {
25462552
log(" -n <integer>\n");
25472553
log(" number of clock cycles to simulate (default: 20)\n");
25482554
log("\n");
2555+
log(" -noinitstate\n");
2556+
log(" do not activate $initstate cells during the first cycle\n");
2557+
log("\n");
25492558
log(" -a\n");
25502559
log(" use all nets in VCD/FST operations, not just those with public names\n");
25512560
log("\n");
@@ -2646,6 +2655,10 @@ struct SimPass : public Pass {
26462655
worker.cycles_set = true;
26472656
continue;
26482657
}
2658+
if (args[argidx] == "-noinitstate") {
2659+
worker.initstate = false;
2660+
continue;
2661+
}
26492662
if (args[argidx] == "-rstlen" && argidx+1 < args.size()) {
26502663
worker.rstlen = atoi(args[++argidx].c_str());
26512664
continue;

0 commit comments

Comments
 (0)