mirror of
https://github.com/YosysHQ/yosys
synced 2025-07-14 08:26:41 +00:00
74 lines
1.1 KiB
Text
74 lines
1.1 KiB
Text
verific -formal <<EOT
|
|
|
|
module top(input clk, a, en);
|
|
reg a_q = '0;
|
|
reg en_q = '0;
|
|
|
|
always @(posedge clk) begin
|
|
a_q <= a;
|
|
en_q <= en;
|
|
end
|
|
|
|
always @(posedge clk)
|
|
if (en_q)
|
|
assert(a_q);
|
|
endmodule
|
|
EOT
|
|
|
|
prep
|
|
|
|
design -save prep
|
|
|
|
select -assert-count 1 t:$assert
|
|
|
|
chformal -assert2assume
|
|
|
|
select -assert-count 1 t:$assume
|
|
|
|
chformal -assume2assert
|
|
|
|
select -assert-count 1 t:$assert
|
|
|
|
async2sync
|
|
|
|
chformal -lower
|
|
select -assert-count 1 t:$assert
|
|
|
|
design -load prep
|
|
|
|
chformal -assert2cover
|
|
|
|
select -assert-count 1 t:$cover
|
|
|
|
design -load prep
|
|
|
|
chformal -assert2assume
|
|
async2sync
|
|
chformal -lower
|
|
chformal -assume -early
|
|
|
|
rename -enumerate -pattern assume_% t:$assume
|
|
expose -evert t:$assume
|
|
|
|
design -save gold
|
|
|
|
design -load prep
|
|
|
|
chformal -assert2assume
|
|
chformal -assume -early
|
|
async2sync
|
|
chformal -lower
|
|
|
|
rename -enumerate -pattern assume_% t:$assume
|
|
expose -evert t:$assume
|
|
|
|
design -save gate
|
|
|
|
design -reset
|
|
|
|
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 -tempinduct miter
|