diff options
| author | Clifford Wolf <clifford@clifford.at> | 2015-08-15 10:50:27 +0200 |
|---|---|---|
| committer | Clifford Wolf <clifford@clifford.at> | 2015-08-15 10:50:27 +0200 |
| commit | ec0891326aee1334bce4bb096e7521a3907d4bdc (patch) | |
| tree | bd11ae7bde286533ba4e0c62951d0c2446dc488b /scripts/smt2-bmc/async.ys | |
| parent | b28e82cb81ae81f648a14a930de9373ed9583e67 (diff) | |
| download | picorv32-ec0891326aee1334bce4bb096e7521a3907d4bdc.tar.gz picorv32-ec0891326aee1334bce4bb096e7521a3907d4bdc.zip | |
Renamed scripts/smt2-bmc/mem_equiv to .../async
Diffstat (limited to 'scripts/smt2-bmc/async.ys')
| -rw-r--r-- | scripts/smt2-bmc/async.ys | 31 |
1 files changed, 31 insertions, 0 deletions
diff --git a/scripts/smt2-bmc/async.ys b/scripts/smt2-bmc/async.ys new file mode 100644 index 0000000..1f7c8f8 --- /dev/null +++ b/scripts/smt2-bmc/async.ys @@ -0,0 +1,31 @@ +read_verilog async.v +read_verilog ../../picorv32.v +rename main main_a +chparam -set ENABLE_REGS_DUALPORT 0 \ + -set TWO_STAGE_SHIFT 0 \ + -set TWO_CYCLE_COMPARE 0 \ + -set TWO_CYCLE_ALU 0 main_a +hierarchy -top main_a +proc +opt +memory -nordff -nomap +flatten +opt +write_smt2 -bv -mem -regs async_a.smt2 +design -reset + +read_verilog async.v +read_verilog ../../picorv32.v +rename main main_b +chparam -set ENABLE_REGS_DUALPORT 1 \ + -set TWO_STAGE_SHIFT 1 \ + -set TWO_CYCLE_COMPARE 1 \ + -set TWO_CYCLE_ALU 1 main_b +hierarchy -top main_b +proc +opt +memory -nordff -nomap +flatten +opt +write_smt2 -bv -mem -regs async_b.smt2 +design -reset |