mirror of
https://github.com/YosysHQ/yosys.git
synced 2026-10-06 01:53:53 +02:00
33 lines
886 B
Plaintext
33 lines
886 B
Plaintext
# FF init on a private output wire must survive write_xaiger2 -mapping_prep
|
|
read_verilog <<EOT
|
|
module top(input clk, input [1:0] a, output [1:0] o);
|
|
reg [1:0] r;
|
|
initial r = 2'b10;
|
|
always @(posedge clk) r <= r + a;
|
|
assign o = ~r;
|
|
endmodule
|
|
EOT
|
|
prep
|
|
rename -hide w:r
|
|
techmap
|
|
opt
|
|
design -save gold
|
|
|
|
abc9 -lut 4
|
|
select -assert-min 1 a:init
|
|
design -stash gate
|
|
design -copy-from gold -as gold top
|
|
design -copy-from gate -as gate top
|
|
miter -equiv -flatten -make_assert gold gate miter
|
|
sat -verify -prove-asserts -seq 3 -set-init-undef -set-def-inputs miter
|
|
|
|
design -load gold
|
|
abc_new -liberty ../liberty/normal.lib
|
|
select -assert-min 1 a:init
|
|
design -stash gate
|
|
design -copy-from gold -as gold top
|
|
design -copy-from gate -as gate top
|
|
read_liberty ../liberty/normal.lib
|
|
miter -equiv -flatten -make_assert gold gate miter
|
|
sat -verify -prove-asserts -seq 3 -set-init-undef -set-def-inputs miter
|