FEV vs. gate-level

[stevehoover]

I'm having a difficult time finding the right command sequence to FEV sequential (stateful) circuits vs. their gate-level implementations. I'm currently getting the following error signature:

ERROR: Failed to import cell $flatten\gate.$procdff$210 (type $dff) to SAT database.

Here's a simple reproducer.

fib.vs:

//  A circuit computing the Fibonacci sequence.
module top(input wire clk, input wire reset, input wire [31:0] cyc_cnt, output wire passed, output wire failed);
   wire [15:0] L0_Val_n1;
   reg  [15:0] L0_Val_a0,
               L0_Val_a1;
   wire L0_reset_a0;

   always @(posedge clk) L0_Val_a0[15:0] <= L0_Val_n1[15:0];
   always @(posedge clk) L0_Val_a1[15:0] <= L0_Val_a0[15:0];

   assign L0_reset_a0 = reset;
   assign L0_Val_n1[15:0] = L0_reset_a0 ? 1 : L0_Val_a0 + L0_Val_a1;

   assign passed = L0_Val_n1 == 16'd21;
   assign failed = cyc_cnt == 32'd30;
endmodule

Synthesize in yosys:

read_verilog -sv fib.sv
synth -top top
write_verilog fib_synth.v
exit

FEV in yosys:

read_verilog -sv fib.sv
rename top top1
proc
memory
flatten top1
hierarchy -top top1
read_verilog fib_synth.v
rename top top2
proc
memory
flatten top2
clean -purge
miter -equiv -make_assert -flatten top1 top2 miter
sat -verify -prove-asserts -enable_undef -max_undef -show-public miter

I'm using Yosys 0.15+11 (and I get the same result with Yosys 0.9).

[nakengelhardt]

If you want to use sat for a circuit with registers in it, you need to pass the -seq N option. For example:

read_verilog -sv fib.sv
hierarchy -top top
proc
clean
design -save gold
synth
design -stash gate
design -copy-from gold -as gold top
design -copy-from gate -as gate top
miter -equiv -make_assert -flatten gold gate miter
sat -verify -seq 2 -prove-asserts -enable_undef miter

[stevehoover]

Thanks, Nina. With input constraints on clk and reset I was able to get this simple circuit to pass FEV. It seems I should try SymbiYosys before moving to bigger circuits.