Для разработки (моделирования) микропроцессоров используется вот такая система (бесплатная) ACL2. По идее с пее помощью можно спроектировать и верифицировать цифровые устройства, пр...

Кто работал с подобной пробграммой? Отпишитесь плиз.
Интересует: описания и литература (кроме офф. сайта конечно); GUI (с PLT+Dracula так и не разобрался...), примеры итд

Имеет ли смысл разбираться в ней? (там все я так понимаю на Лиспе надо описывать...)
Какую бы коммерческую альтернативу вы порекомендовали? На сколько эффективней такой подход в разработке чем например описание на VHDL или Verilog и отладке в таких программах как ActiveHDL итд?

Спасибо!